Metamath Proof Explorer Home Metamath Proof Explorer
Most Recent Proofs
 
Mirrors  >  Home  >  MPE Home  >  Th. List  >  Recent Other  >  MM 100

Most recent proofs    These are the 10 (GIF, Unicode) or 1000 (GIF, Unicode) most recent proofs in the set.mm database for the Metamath Proof Explorer (and the Hilbert Space Explorer). The set.mm database is maintained on Github with master (stable) and develop (development) versions. This page was created from develop commit afb80ca, also available here: set.mm (30MB) or set.mm.bz2 (compressed, 8MB).

Other links    Email: Norm Megill.    Mailing list: Metamath Google Group Updated 22-Apr-2017 .    Syndication: RSS feed (courtesy of Dan Getz).    Related wikis: Wikiproofs (JHilbert) (Recent Changes); Ghilbert site; Ghilbert Google Group.

Recent news items    (13-Apr-2017) See equidK for a discussion of the recent theorems in my mathbox. -NM

(24-Mar-2017) Alan Sare updated his completeusersproof program.

(28-Feb-2017) David Moews added a new proof to the 100 theorem list, Product of Segments of Chords chordthm, bringing the Metamath total to 62.

(18-Feb-2017) Filip Cernatescu announced Milpgame 0.1 (MILP: Math is like a puzzle!).

(1-Jan-2017) Saveliy Skresanov added a new proof to the 100 theorem list, Isosceles triangle theorem isosctr, bringing the Metamath total to 61.

(1-Jan-2017) Mario Carneiro added 2 new proofs to the 100 theorem list, L'Hôpital's Rule lhop and Taylor's Theorem taylth, bringing the Metamath total to 60.

(28-Dec-2016) David A. Wheeler is putting together a page on Metamath (specifically set.mm) conventions. Comments are welcome on the Google Group thread.

(24-Dec-2016) Mario Carneiro introduced the abbreviation "F/ x ph" (symbols: turned F, x, phi) in df-nf to represent the "effectively not free" idiom "A. x ( ph -> A. x ph )". Theorem nf2 shows a version without nested quantifiers.

(22-Dec-2016) Naip Moro has developed a Metamath database for G. Spencer-Brown's Laws of Form. You can follow the Google Group discussion here.

(20-Dec-2016) In metamath program version 0.137, 'verify markup *' now checks that ax-XXX $a matches axXXX $p when the latter exists, per the discussion at https://groups.google.com/d/msg/metamath/Vtz3CKGmXnI/Fxq3j1I_EQAJ.

(24-Nov-2016) Mingl Yuan has kindly provided a mirror site in Beijing, China. He has also provided an rsync server; type "rsync cn.metamath.org::" in a bash shell to check its status (it should return "metamath metamath").

(14-Aug-2016) All HTML pages on this site should now be mobile-friendly and pass the Mobile-Friendly Test. If you find one that does not, let me know.

(14-Aug-2016) Daniel Whalen wrote a paper describing the use of using deep learning to prove 14% of test theorems taken from set.mm: Holophrasm: a neural Automated Theorem Prover for higher-order logic. The associated program is called Holophrasm.

(14-Aug-2016) David A. Wheeler created a video called Metamath Proof Explorer: A Modern Principia Mathematica

(12-Aug-2016) A Gitter chat room has been created for Metamath.

(9-Aug-2016) Mario Carneiro wrote a Metamath proof verifier in the Scala language as part of the ongoing Metamath -> MMT import project

(9-Aug-2016) David A. Wheeler created a GitHub project called metamath-test (last execution run) to check that different verifiers both pass good databases and detect errors in defective ones.

(4-Aug-2016) Mario gave two presentations at CICM 2016.

(17-Jul-2016) Thierry Arnoux has written EMetamath, a Metamath plugin for the Eclipse IDE.

(16-Jul-2016) Mario recovered Chris Capel's collapsible proof demo.

(13-Jul-2016) FL sent me an updated version of PDF (LaTeX source) developed with Lamport's pf2 package. See the 23-Apr-2012 entry below.

(12-Jul-2016) David A. Wheeler produced a new video for mmj2 called "Creating functions in Metamath". It shows a more efficient approach than his previous recent video "Creating functions in Metamath" (old) but it can be of interest to see both approaches.

(10-Jul-2016) Metamath program version 0.132 changes the command 'show restricted' to 'show discouraged' and adds a new command, 'set discouragement'. See the mmnotes.txt entry of 11-May-2016 (updated 10-Jul-2016).

(12-Jun-2016) Dan Getz has written Metamath.jl, a Metamath proof verifier written in the Julia language.    Older news...

Color key:   Metamath Proof Explorer  Metamath Proof Explorer   Hilbert Space Explorer  Hilbert Space Explorer   User Mathboxes  User Mathboxes  

Last updated on 23-Apr-2017 at 6:19 AM ET.
Recent Additions to the Metamath Proof Explorer   Notes (last updated 10-Jul-16 )
DateLabelDescription
Theorem
 
21-Apr-2017ax12olem24K 27879 Lemma for ax12o 1663. Construct an intermediate equivalent to ax-12 1633 from two instances of ax-12 1633. Uses only Tarski's FOL axiom schemes (see description for equidK 27792). Note that  x and  y are bundled. THIS IS AS FAR AS I WAS ABLE TO GET using only Tarski's schemes; I couldn't find a way to prove ax12olem25 1659 through ax12olem27 1661 without making  x and  y distinct. (Contributed by NM, 21-Apr-2017.) (New usage is discouraged.)
 |-  ( -.  x  =  y  ->  ( y  =  z 
 ->  A. x  y  =  z ) )   &    |-  ( -.  x  =  y  ->  ( y  =  w 
 ->  A. x  y  =  w ) )   =>    |-  ( -.  x  =  y  ->  ( -. 
 A. x  -.  y  =  z  ->  A. x  y  =  z )
 )
 
20-Apr-2017ax12olem22K 27875 Lemma for ax12o 1663. Negate the equalities in ax-12 1633, shown as the hypothesis. Uses only Tarski's FOL axiom schemes (see description for equidK 27792). Note that  x and  y are bundled. (Contributed by NM, 20-Apr-2017.) (New usage is discouraged.)
 |-  ( -.  x  =  y  ->  ( y  =  w 
 ->  A. x  y  =  w ) )   =>    |-  ( -.  x  =  y  ->  ( -.  y  =  z  ->  A. x  -.  y  =  z ) )
 
20-Apr-2017equextvK 27874 An extensionality-like property for equality. Similar to equveli 1880. Uses only Tarski's FOL axiom schemes (see description for equidK 27792). Note that  x and  y are bundled. (Contributed by NM, 20-Apr-2017.)
 |-  ( x  =  y  <->  A. z ( z  =  x  <->  z  =  y
 ) )
 
20-Apr-2017equvinvK 27861 Similar to equvini 1879. Uses only Tarski's FOL axiom schemes (see description for equidK 27792). Note that  x and  y are bundled. (Contributed by NM, 20-Apr-2017.)
 |-  ( x  =  y  <->  E. z ( x  =  z  /\  z  =  y ) )
 
19-Apr-2017ax12olem23aK 27877 Lemma for ax12o 1663. Show one direction of the equivalence of an intermediate equivalent to ax-12o 1664 with the conjunction of ax-12 1633 and a variant with negated equalities. Uses only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.)
 |-  (
 ( ( -.  x  =  y  ->  ( y  =  z  ->  A. x  y  =  z )
 )  /\  ( -.  x  =  y  ->  ( -.  y  =  z 
 ->  A. x  -.  y  =  z ) ) ) 
 ->  ( -.  x  =  y  ->  ( -.  A. x  -.  y  =  z  ->  A. x  y  =  z ) ) )
 
19-Apr-2017ax12olem21K 27872 Lemma for ax12o 1663. Similar to equvin 1999 but with a negated equality. Uses only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.)
 |-  ( E. w ( y  =  w  /\  -.  z  =  w )  <->  -.  y  =  z )
 
19-Apr-2017ax12olem20K 27870 Lemma for ax12o 1663. Weak version of 19.12 1766, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.)
 |-  (
 y  =  w  ->  ( ph  <->  ch ) )   =>    |-  ( E. x A. y ph  ->  A. y E. x ph )
 
19-Apr-2017ax12olem19K 27868 Lemma for ax12o 1663. Weak version of nfex 1733, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.)
 |-  ( x  =  w  ->  (
 ph 
 <->  ps ) )   &    |-  ( ph  ->  A. x ph )   =>    |-  ( E. y ph  ->  A. x E. y ph )
 
19-Apr-2017ax12olem18K 27866 Lemma for ax12o 1663. Weak version of hbim1 1810, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.)
 |-  ( x  =  w  ->  (
 ph 
 <->  ch ) )   &    |-  ( x  =  w  ->  ( ps  <->  ta ) )   &    |-  ( ph  ->  A. x ph )   &    |-  ( ph  ->  ( ps  ->  A. x ps ) )   =>    |-  ( ( ph  ->  ps )  ->  A. x (
 ph  ->  ps ) )
 
19-Apr-2017ax12olem17K 27864 Lemma for ax12o 1663. Weak version of 19.21 1771, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.)
 |-  ( x  =  w  ->  (
 ph 
 <->  ch ) )   &    |-  ( x  =  w  ->  ( ps  <->  ta ) )   &    |-  ( ph  ->  A. x ph )   =>    |-  ( A. x ( ph  ->  ps )  <->  ( ph  ->  A. x ps ) )
 
19-Apr-2017ax12olem16K 27862 Lemma for ax12o 1663. Weak version of equsalh 1851, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.)
 |-  ( x  =  w  ->  ( ps  <->  ta ) )   &    |-  ( ps  ->  A. x ps )   &    |-  ( x  =  y  ->  (
 ph 
 <->  ps ) )   =>    |-  ( A. x ( x  =  y  -> 
 ph )  <->  ps )
 
19-Apr-2017ax12o10lem15K 27859 Lemma for ax12o 1663. Weak version of exlimih 1782, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.)
 |-  ( x  =  w  ->  (
 ph 
 <->  ch ) )   &    |-  ( x  =  w  ->  ( ps  <->  ta ) )   &    |-  ( ps  ->  A. x ps )   &    |-  ( ph  ->  ps )   =>    |-  ( E. x ph  ->  ps )
 
19-Apr-2017ax12o10lem14K 27857 Lemma for ax12o 1663. Weak version of 19.23 1777, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.)
 |-  ( x  =  w  ->  (
 ph 
 <->  ch ) )   &    |-  ( x  =  w  ->  ( ps  <->  ta ) )   &    |-  ( ps  ->  A. x ps )   =>    |-  ( A. x ( ph  ->  ps )  <->  ( E. x ph 
 ->  ps ) )
 
19-Apr-2017ax12o10lem13K 27855 Lemma for ax12o 1663. Weak version of 19.9 1762, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.)
 |-  ( x  =  w  ->  (
 ph 
 <->  ps ) )   &    |-  ( ph  ->  A. x ph )   =>    |-  ( E. x ph  <->  ph )
 
19-Apr-2017ax12o10lem12K 27853 Lemma for ax12o 1663. Weak version of 19.9t 1761, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.)
 |-  ( x  =  w  ->  (
 ph 
 <->  ps ) )   =>    |-  ( A. x ( ph  ->  A. x ph )  ->  ( E. x ph 
 ->  ph ) )
 
19-Apr-2017ax12o10lem11K 27851 Lemma for ax12o 1663. Weak version of hbim 1723, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.)
 |-  ( x  =  w  ->  (
 ph 
 <->  ch ) )   &    |-  ( ph  ->  A. x ph )   &    |-  ( ps  ->  A. x ps )   =>    |-  (
 ( ph  ->  ps )  ->  A. x ( ph  ->  ps ) )
 
19-Apr-2017ax12o10lem10K 27848 Lemma for ax12o 1663. Weak version of hbnt 1717, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.)
 |-  ( x  =  w  ->  (
 ph 
 <->  ps ) )   =>    |-  ( A. x ( ph  ->  A. x ph )  ->  ( -.  ph  ->  A. x  -.  ph ) )
 
19-Apr-2017ax12o10lem9K 27847 Lemma for ax12o 1663. Weak version of ax6o 1696, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.)
 |-  ( x  =  w  ->  (
 ph 
 <->  ps ) )   =>    |-  ( -.  A. x  -.  A. x ph  -> 
 ph )
 
19-Apr-2017ax12o10lem8K 27845 Lemma for ax12o 1663 and ax10 1677. Weak version of a4ime 1868 with distinct variables, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.)
 |-  ( x  =  w  ->  (
 ph 
 <-> 
 th ) )   &    |-  ( x  =  w  ->  ( ps  <->  ta ) )   &    |-  ( x  =  z  ->  (
 ph  ->  ps ) )   &    |-  ( ph  ->  A. x ph )   =>    |-  ( ph  ->  E. x ps )
 
19-Apr-2017ax12o10lem7K 27843 Lemma for ax12o 1663 and ax10 1677. Weak version of hbimd 1809, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.)
 |-  ( x  =  w  ->  ( ps  <->  th ) )   &    |-  ( ph  ->  A. x ph )   &    |-  ( ph  ->  ( ps  ->  A. x ps ) )   &    |-  ( ph  ->  ( ch  ->  A. x ch )
 )   =>    |-  ( ph  ->  (
 ( ps  ->  ch )  ->  A. x ( ps 
 ->  ch ) ) )
 
19-Apr-2017ax12o10lem6K 27841 Lemma for ax12o 1663 and ax10 1677. Weak version of hbn 1722, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.)
 |-  ( x  =  w  ->  (
 ph 
 <->  ps ) )   &    |-  ( ph  ->  A. x ph )   =>    |-  ( -.  ph  ->  A. x  -.  ph )
 
19-Apr-2017ax12o10lem5K 27839 Lemma for ax12o 1663 and ax10 1677. Weak version of hba1 1718, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.)
 |-  ( x  =  w  ->  (
 ph 
 <->  ps ) )   =>    |-  ( A. x ph 
 ->  A. x A. x ph )
 
19-Apr-2017ax12o10lem4K 27837 Lemma for ax12o 1663. Weak version of 19.8a 1758, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.)
 |-  ( x  =  w  ->  (
 ph 
 <->  ps ) )   =>    |-  ( ph  ->  E. x ph )
 
19-Apr-2017ax12o10lem3K 27836 Lemma for ax12o 1663 and ax10 1677. Weak version of ax4 1691, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.)
 |-  ( x  =  w  ->  (
 ph 
 <->  ps ) )   =>    |-  ( A. x ph 
 ->  ph )
 
19-Apr-2017ax11wflemK 27822 Verson of ax11wlemK 27823 without distinct variables. (Contributed by NM, 19-Apr-2017.)
 |-  ( ps  ->  A. x ps )   &    |-  ( x  =  y  ->  (
 ph 
 <->  ps ) )   =>    |-  ( x  =  y  ->  ( ph  ->  A. x ( x  =  y  ->  ph )
 ) )
 
19-Apr-2017hbalwK 27820 Weak version of hbal 1567. Uses only Tarski's predicate calculus axiom schemes i.e. does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633, and uses ax-9v 1632 instead of ax-9 1684. Unlike hbal 1567, this theorem requires that  x and  y be distinct i.e. are not bundled. (Contributed by NM, 19-Apr-2017.)
 |-  ( x  =  z  ->  (
 ph 
 <->  ps ) )   &    |-  ( ph  ->  A. x ph )   =>    |-  ( A. y ph  ->  A. x A. y ph )
 
19-Apr-2017hbe1wK 27818 Weak version of hbe1 1565. See comments for ax6wK 27816. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. (Contributed by NM, 19-Apr-2017.)
 |-  ( x  =  y  ->  (
 ph 
 <->  ps ) )   =>    |-  ( E. x ph 
 ->  A. x E. x ph )
 
19-Apr-2017ax6wfK 27815 Weak version of ax-6 1534 from which we can prove any ax-6 1534 instance not involving wff variables or bundling. Uses only Tarski's predicate calculus axiom schemes i.e. does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633, and uses ax-9v 1632 instead of ax-9 1684. See the description in the comment of equidK 27792. (Contributed by NM, 19-Apr-2017.)
 |-  ( A. x ph  ->  A. y A. x ph )   &    |-  ( -.  ps  ->  A. x  -.  ps )   &    |-  ( A. y ps  ->  A. x A. y ps )   &    |-  ( -.  ph  ->  A. y  -.  ph )   &    |-  ( -.  A. y ps  ->  A. x  -.  A. y ps )   &    |-  ( x  =  y  ->  ( ph  <->  ps ) )   =>    |-  ( -.  A. x ph 
 ->  A. x  -.  A. x ph )
 
19-Apr-2017cbvexvK 27814 Change bound variable. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. (Contributed by NM, 19-Apr-2017.)
 |-  ( x  =  y  ->  (
 ph 
 <->  ps ) )   =>    |-  ( E. x ph  <->  E. y ps )
 
19-Apr-2017cbvaliK 27810 Change bound variable. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. Part of Lemma 7 of [KalishMontague] p. 86. (Contributed by NM, 19-Apr-2017.)
 |-  ( A. x ph  ->  A. y A. x ph )   &    |-  ( -.  ps  ->  A. x  -.  ps )   &    |-  ( x  =  y  ->  ( ph  ->  ps ) )   =>    |-  ( A. x ph 
 ->  A. y ps )
 
19-Apr-2017ax4wfK 27806 Weak version of ax-4 1692. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. Lemma 9 of [KalishMontague] p. 86. This may be the best we can do with minimal distinct variable conditions. (Contributed by NM, 19-Apr-2017.)
 |-  ( -.  ps  ->  A. x  -.  ps )   &    |-  ( A. x ph 
 ->  A. y A. x ph )   &    |-  ( -.  ph  ->  A. y  -.  ph )   &    |-  ( x  =  y 
 ->  ( ph  <->  ps ) )   =>    |-  ( A. x ph 
 ->  ph )
 
19-Apr-2017a4imK 27804 Specialization. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. Lemma 8 of [KalishMontague] p. 87. (Contributed by NM, 19-Apr-2017.)
 |-  ( -.  ps  ->  A. x  -.  ps )   &    |-  ( x  =  y  ->  ( ph  ->  ps ) )   =>    |-  ( A. x ph 
 ->  ps )
 
19-Apr-2017albidK 27802 Add universal quantifier to both sides of an equivalence. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. (Contributed by NM, 19-Apr-2017.)
 |-  ( ph  ->  A. x ph )   &    |-  ( ph  ->  ( ps  <->  ch ) )   =>    |-  ( ph  ->  (
 A. x ps  <->  A. x ch )
 )
 
19-Apr-2017alimdK 27800 Add universal quantifier to both sides of an equivalence. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. Part of Lemma 5 of [KalishMontague] p. 86. (The other parts are just notbii 289 and imbi12i 318.) (Contributed by NM, 19-Apr-2017.)
 |-  ( ph  ->  A. x ph )   &    |-  ( ph  ->  ( ps  ->  ch ) )   =>    |-  ( ph  ->  ( A. x ps  ->  A. x ch ) )
 
14-Apr-2017ax11wdemoK 27826 Example of an application of ax11wK 27824 that results in an instance of ax-11 1624 for a contrived formula with mixed free and bound variables,  ( x  e.  y  /\  A. x
z  e.  x  /\  A. y A. z y  e.  x ), in place of  ph. The proof illustrates bound variable renaming with cbvalvK 27813 to obtain fresh variables to avoid distinct variable clashes. Uses only Tarski's predicate calculus axiom schemes i.e. does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633, and uses ax-9v 1632 instead of ax-9 1684. See the description in the comment of equidK 27792. (Contributed by NM, 14-Apr-2017.)
 |-  ( x  =  y  ->  (
 A. y ( x  e.  y  /\  A. x  z  e.  x  /\  A. y A. z  y  e.  x )  ->  A. x ( x  =  y  ->  ( x  e.  y  /\  A. x  z  e.  x  /\  A. y A. z  y  e.  x )
 ) ) )
 
13-Apr-2017ax12dgen4K 27831 Degenerate instance of ax-12 1633 where bundled variables  x,  y, and  z have a common substitution. Uses only Tarski's predicate calculus axiom schemes i.e. does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633, and uses ax-9v 1632 instead of ax-9 1684. See the description in the comment of equidK 27792. (Contributed by NM, 13-Apr-2017.)
 |-  ( -.  x  =  x  ->  ( x  =  x 
 ->  A. x  x  =  x ) )
 
13-Apr-2017ax12dgen3K 27830 Degenerate instance of ax-12 1633 where bundled variables  y and  z have a common substitution. Uses only Tarski's predicate calculus axiom schemes i.e. does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633, and uses ax-9v 1632 instead of ax-9 1684. See the description in the comment of equidK 27792. (Contributed by NM, 13-Apr-2017.)
 |-  ( -.  x  =  y  ->  ( y  =  y 
 ->  A. x  y  =  y ) )
 
13-Apr-2017ax12dgen2K 27829 Degenerate instance of ax-12 1633 where bundled variables  x and  z have a common substitution. Uses only Tarski's predicate calculus axiom schemes i.e. does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633, and uses ax-9v 1632 instead of ax-9 1684. See the description in the comment of equidK 27792. (Contributed by NM, 13-Apr-2017.)
 |-  ( -.  x  =  y  ->  ( y  =  x 
 ->  A. x  y  =  x ) )
 
13-Apr-2017ax12dgen1K 27828 Degenerate instance of ax-12 1633 where bundled variables  x and  y have a common substitution. Uses only Tarski's predicate calculus axiom schemes i.e. does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633, and uses ax-9v 1632 instead of ax-9 1684. See the description in the comment of equidK 27792. (Contributed by NM, 13-Apr-2017.)
 |-  ( -.  x  =  x  ->  ( x  =  z 
 ->  A. x  x  =  z ) )
 
13-Apr-2017ax11dgenK 27825 Degenerate instance of ax-11 1624 where bundled variables  x and  y have a common substitution. Uses only Tarski's predicate calculus axiom schemes i.e. does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633, and uses ax-9v 1632 instead of ax-9 1684. See the description in the comment of equidK 27792. (Contributed by NM, 13-Apr-2017.)
 |-  ( x  =  x  ->  (
 A. x ph  ->  A. x ( x  =  x  ->  ph ) ) )
 
13-Apr-2017ax7dgenK 27821 Degenerate instance of ax-7 1535 where bundled variables  x and  y have a common substitution. Uses only Tarski's predicate calculus axiom schemes i.e. does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633, and uses ax-9v 1632 instead of ax-9 1684. See the description in the comment of equidK 27792. (Contributed by NM, 13-Apr-2017.)
 |-  ( A. x A. x ph  ->  A. x A. x ph )
 
11-Apr-2017albidvK 27803 Add universal quantifier to both sides of an equivalence. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. (Contributed by NM, 11-Apr-2017.)
 |-  ( ph  ->  ( ps  <->  ch ) )   =>    |-  ( ph  ->  (
 A. x ps  <->  A. x ch )
 )
 
11-Apr-2017alimdvK 27801 Add universal quantifier to both sides of an equivalence. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. Part of Lemma 5 of [KalishMontague] p. 86. (The other parts are just notbii 289 and imbi12i 318.) (Contributed by NM, 11-Apr-2017.)
 |-  ( ph  ->  ( ps  ->  ch ) )   =>    |-  ( ph  ->  ( A. x ps  ->  A. x ch ) )
 
10-Apr-2017ax12wK 27827 Weak version (principal instance) of ax-12 1633 not involving bundling. Uses only Tarski's predicate calculus axiom schemes. The proof is trivial but is included to complete the set ax6wK 27816, ax7wK 27819, and ax11wK 27824. See the description in the comment of equidK 27792. (Contributed by NM, 10-Apr-2017.)
 |-  ( -.  x  =  y  ->  ( y  =  z 
 ->  A. x  y  =  z ) )
 
10-Apr-2017ax11wK 27824 Weak version of ax-11 1624 from which we can prove any ax-7 1535 instance not involving wff variables or bundling. Uses only Tarski's predicate calculus axiom schemes i.e. does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633, and uses ax-9v 1632 instead of ax-9 1684. An instance of the first hypothesis will normally require that  x and  y be distinct (unless  x does not occur in  ph). See the description in the comment of equidK 27792. (Contributed by NM, 10-Apr-2017.)
 |-  ( x  =  y  ->  (
 ph 
 <->  ps ) )   &    |-  (
 y  =  z  ->  ( ph  <->  ch ) )   =>    |-  ( x  =  y  ->  ( A. y ph  ->  A. x ( x  =  y  ->  ph ) ) )
 
10-Apr-2017ax11wlemK 27823 Lemma for weak version of ax-11 1624. Uses only Tarski's predicate calculus axiom schemes i.e. does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633, and uses ax-9v 1632 instead of ax-9 1684. In some cases, this lemma may lead to shorter proofs than ax11wK 27824. (Contributed by NM, 10-Apr-2017.)
 |-  ( x  =  y  ->  (
 ph 
 <->  ps ) )   =>    |-  ( x  =  y  ->  ( ph  ->  A. x ( x  =  y  ->  ph )
 ) )
 
10-Apr-2017ax7wK 27819 Weak version of ax-7 1535 from which we can prove any ax-7 1535 instance not involving wff variables or bundling. Uses only Tarski's predicate calculus axiom schemes i.e. does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633, and uses ax-9v 1632 instead of ax-9 1684. Unlike ax-7 1535, this theorem requires that  x and  y be distinct i.e. are not bundled. See the description in the comment of equidK 27792. (Contributed by NM, 10-Apr-2017.)
 |-  (
 y  =  z  ->  ( ph  <->  ps ) )   =>    |-  ( A. x A. y ph  ->  A. y A. x ph )
 
10-Apr-201719.8vK 27809 Version of 19.8a 1758 and its converse when  x does not occur in  ph. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. (Contributed by NM, 10-Apr-2017.)
 |-  ( ph 
 <-> 
 E. x ph )
 
10-Apr-2017ax4vK 27808 Version of ax-4 1692 when  x does not occur in  ph. This provides the other direction of ax-17 1628. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. (Contributed by NM, 10-Apr-2017.)
 |-  ( A. x ph  ->  ph )
 
9-Apr-2017hba1wK 27817 Weak version of hba1 1718. See comments for ax6wK 27816. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. (Contributed by NM, 9-Apr-2017.)
 |-  ( x  =  y  ->  (
 ph 
 <->  ps ) )   =>    |-  ( A. x ph 
 ->  A. x A. x ph )
 
9-Apr-2017ax6wK 27816 Weak version of ax-6 1534 from which we can prove any ax-6 1534 instance not involving wff variables or bundling. Uses only Tarski's predicate calculus axiom schemes i.e. does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633, and uses ax-9v 1632 instead of ax-9 1684. See the description in the comment of equidK 27792. (Contributed by NM, 9-Apr-2017.)
 |-  ( x  =  y  ->  (
 ph 
 <->  ps ) )   =>    |-  ( -.  A. x ph  ->  A. x  -.  A. x ph )
 
9-Apr-2017cbvalvK 27813 Change bound variable. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. (Contributed by NM, 9-Apr-2017.)
 |-  ( x  =  y  ->  (
 ph 
 <->  ps ) )   =>    |-  ( A. x ph  <->  A. y ps )
 
9-Apr-2017cbvalK 27812 Change bound variable. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. (Contributed by NM, 9-Apr-2017.)
 |-  ( A. x ph  ->  A. y A. x ph )   &    |-  ( -.  ps  ->  A. x  -.  ps )   &    |-  ( A. y ps  ->  A. x A. y ps )   &    |-  ( -.  ph  ->  A. y  -.  ph )   &    |-  ( x  =  y 
 ->  ( ph  <->  ps ) )   =>    |-  ( A. x ph  <->  A. y ps )
 
9-Apr-2017cbvalivK 27811 Change bound variable. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. Part of Lemma 7 of [KalishMontague] p. 86. (Contributed by NM, 9-Apr-2017.)
 |-  ( x  =  y  ->  (
 ph  ->  ps ) )   =>    |-  ( A. x ph 
 ->  A. y ps )
 
9-Apr-2017ax4wK 27807 Weak version of ax-4 1692. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. Lemma 9 of [KalishMontague] p. 86. (Contributed by NM, 9-Apr-2017.)
 |-  ( x  =  y  ->  (
 ph 
 <->  ps ) )   =>    |-  ( A. x ph 
 ->  ph )
 
9-Apr-2017a4imvK 27805 Specialization. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. Lemma 8 of [KalishMontague] p. 87. (Contributed by NM, 9-Apr-2017.)
 |-  ( x  =  y  ->  (
 ph  ->  ps ) )   =>    |-  ( A. x ph 
 ->  ps )
 
9-Apr-2017albiiK 27799 Add universal quantifier to both sides of an equivalence. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. Part of Lemma 5 of [KalishMontague] p. 86. (The other parts are just notbii 289 and imbi12i 318.) (Contributed by NM, 9-Apr-2017.)
 |-  ( ph 
 <->  ps )   =>    |-  ( A. x ph  <->  A. x ps )
 
9-Apr-2017alimiK 27798 Add universal quantifier to both sides of an implication. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. (Contributed by NM, 9-Apr-2017.)
 |-  ( ph  ->  ps )   =>    |-  ( A. x ph  ->  A. x ps )
 
9-Apr-2017elequ2K 27797 An equality for the membership predicate. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. (Contributed by NM, 9-Apr-2017.)
 |-  ( x  =  y  ->  ( z  e.  x  <->  z  e.  y
 ) )
 
9-Apr-2017elequ1K 27796 An equality law for the membership predicate. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. (Contributed by NM, 9-Apr-2017.)
 |-  ( x  =  y  ->  ( x  e.  z  <->  y  e.  z
 ) )
 
9-Apr-2017equequ2K 27795 An equality law for equality. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. (Contributed by NM, 9-Apr-2017.)
 |-  ( x  =  y  ->  ( z  =  x  <->  z  =  y
 ) )
 
9-Apr-2017equequ1K 27794 An equality law for equality. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. (Contributed by NM, 9-Apr-2017.)
 |-  ( x  =  y  ->  ( x  =  z  <->  y  =  z
 ) )
 
9-Apr-2017equcomiK 27793 Commutative law for equality. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. Lemma 3 of [KalishMontague] p. 85. (Contributed by NM, 9-Apr-2017.)
 |-  ( x  =  y  ->  y  =  x )
 
9-Apr-2017equidK 27792 (Theorems equidK 27792 through ax12dgen4K 27831 are part of a study of our non-Tarski predicate calculus axiom schemes. We are using this theorem as a placeholder to describe this study.)

The orginal axiom schemes of Tarski's predicate calculus are ax-5 1533, ax-8 1623, ax-9v 1632, ax-13 1625, ax-14 1626, and ax-17 1628 (see http://us.metamath.org/mpegif/mmset.html#compare) and are shown as axiom schemes B4 through B8 in [KalishMontague] p. 81. These are shown to be logically complete by Theorem 1 of [KalishMontague] p. 85.

The axiom system of set.mm includes the additional axiom schemes ax-6 1534, ax-7 1535, ax-11 1624, and ax-12 1633, which are not part of Tarski's axiom schemes. They are used (and we conjecture are required) to make our system "metalogically complete" i.e. able to prove directly all possible schemes with wff and set metavariables, bundled or not, whose object-language instances are valid. (ax-11 1624 has been proved to be required; see http://us.metamath.org/award2003.html#9a. Metalogical independence of the other three are open problems.)

(There arem additional predicate calculus axiom schemes included in set.mm such as ax-4 1692, but they can all be proved as theorems from the above.)

Terminology: Two set (individual) metavariables are "bundled" in an axiom or theorem scheme when there is no distinct variable constraint ($d) imposed on them. (The term "bundled" is due to Raph Levien.) For example, the  x and  y in ax-9 1684 are bundled, but they are not in ax-9v 1632. We also say that a scheme is bundled when it has at least one pair of bundled set metavariables. If distinct variable conditions are added to all set metavariable pairs in a bundled scheme, we call that the "principal" instance of the bundled scheme. For example, ax-9v 1632 is the principal instance of ax-9 1684. Whenever a common variable is substituted for two or more bundled variables in an axiom or theorem scheme, we call the substitution instance "degenerate". For example, the instance  -.  A. x -.  x  =  x of ax-9 1684 is degenerate. An advantage of bundling is ease of use since there are fewer distinct variable restrictions ($d) to be concerned with. There is also a small economy in being able to state principal and degenerate instances simultaneously. A disadvantage is that bundling may present difficulties in translations to other proof languages, which typically lack the concept (in part because their variables often represent the variables of the object language rather than metavariables ranging over them).

Because Tarski's axiom schemes are logically complete, they can be used to prove any object-language instance of ax-6 1534, ax-7 1535, ax-11 1624, and ax-12 1633. "Translating" this to Metamath, it means that Tarksi's axioms can prove any substitution instance of ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633 in which (1) there are no wff metavariables and (2) all set metavariables are mutually distinct i.e. are not bundled. In effect this is mimicking the object language by pretending that each set metavariable is an object-language variable. (There may also be specific instances with wff metavariables and/or bundling that are directly provable from Tarski's axiom schemes, but it isn't guaranteed. Whether all of them are possible is part of the still open metalogical independence problem for our additional axiom schemes.)

It can be useful to see how this can be done, both to show that our additional schemes are valid metatheorems of Tarski's system and to be able to translate object language instances of our proofs into proofs that would work with a system using only Tarski's original schemes. In addition, it may (or may not) provide insight into the conjectured metalogical independence of our additional schemes.

Past work showed that instances of ax-11o 1940 meeting condition (1) can be proved without invoking that axiom scheme (see comments in ax-11 1624). However, it was somewhat awkward to use, involving an inductive argument with auxiliary theorems ax11eq 2105, ax11el 2106, ax11indn 2108, ax11indi 2109, and ax11inda 2113. It also used axiom schemes other than Tarski's.

The new theorem schemes ax6wK 27816, ax7wK 27819, ax11wK 27824, and ax12wK 27827 are derived using only Tarski's axiom schemes, showing that Tarski's schemes can be used to derive all substitution instances of ax-6 1534, ax-7 1535, ax-11 1624, and ax-12 1633 meeting conditions (1) and (2). (The "K" suffix stands for Kalish/Montague, whose paper was a source for some of the proofs. I may change these names in the future since our practice has been to reserve upper case for special cases such as the ALT or OLD suffixes.) Each hypothesis of ax6wK 27816, ax7wK 27819, and ax11wK 27824 is of the form  ( x  =  y  ->  ( ph  <->  ps ) ) where  ps is an auxiliary or "dummy" wff metavariable in which  x doesn't occur. We can show by induction on formula length that the hypotheses can be eliminated in all cases meeting conditions (1) and (2). The example ax11wdemoK 27826 illustrates the techniques (equality theorems and bound variable renaming) used to achieve this.

We also show the degenerate instances for axioms with bundled variables in ax7dgenK 27821, ax11dgenK 27825, ax12dgen1K 27828, ax12dgen2K 27829, ax12dgen3K 27830, and ax12dgen4K 27831. (Their proofs are trivial but we include them to be thorough.) Combining the principal and degenerate cases outside of Metamath, we show that the bundled schemes ax-6 1534, ax-7 1535, ax-11 1624, and ax-12 1633 are schemes of Tarski's system, meaning that all object language instances they generate are theorems of Tarski's system.

It is interesting that Tarski's system bundles set metavariables in ax-8 1623, ax-13 1625, and ax-14 1626; indeed, a degenerate instance of ax-8 1623 appears to be indispensable for the proof of equidK 27792. Perhaps his general philosophy was that bundling is acceptable for free variables. But he also used the bundled scheme ax-9 1684 in an older system, so it seems the main purpose of his later ax-9v 1632 was just to show that the weaker unbundled form is sufficient rather than an aesthetic objection to bundled free and bound variables.

The case of ax-4 1692 is curious: originally an axiom of Tarski's system, it was proved redundant by Lemma 9 of [KalishMontague] p. 86. However, the proof is by induction on formula length, and the compact scheme form  A. x ph  ->  ph apparently cannot be proved directly from Tarski's other axioms. The best we can do seems to be ax4wK 27807, again requiring substitution instances of  ph that meet conditions (1) and (2) above. Note that our direct proof ax4 1691 requires ax-11 1624, which is not part of Tarski's system.

(End of study description.)

Identity law for equality. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. Lemma 2 of [KalishMontague] p. 85. (Contributed by NM, 9-Apr-2017.)

 |-  x  =  x
 
28-Feb-2017chordthm 19878 The intersecting chords theorem. If points A, B, C, and D lie on a circle (with center Q, say), and the point P is on the interior of the segments AB and CD, then the two products of lengths PA  x. PB and PC  x. PD are equal. The Euclidean plane is identified with the complex plane, and the fact that P is on AB and on CD is expressed by the hypothesis that the angles APB and CPD are equal to  pi. The result is proven by using chordthmlem5 19877 twice to show that PA  x. PB and PC  x. PD both equal BQ2  - PQ2. This is similar to the proof of the theorem given in Euclid's Elements, where it is Proposition III.35. (Contributed by David Moews, 28-Feb-2017.)
 |-  F  =  ( x  e.  ( CC  \  { 0 } ) ,  y  e.  ( CC  \  { 0 } )  |->  ( Im `  ( log `  ( y  /  x ) ) ) )   &    |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  D  e.  CC )   &    |-  ( ph  ->  P  e.  CC )   &    |-  ( ph  ->  A  =/=  P )   &    |-  ( ph  ->  B  =/=  P )   &    |-  ( ph  ->  C  =/=  P )   &    |-  ( ph  ->  D  =/=  P )   &    |-  ( ph  ->  ( ( A  -  P ) F ( B  -  P ) )  =  pi )   &    |-  ( ph  ->  ( ( C  -  P ) F ( D  -  P ) )  =  pi )   &    |-  ( ph  ->  Q  e.  CC )   &    |-  ( ph  ->  ( abs `  ( A  -  Q ) )  =  ( abs `  ( B  -  Q ) ) )   &    |-  ( ph  ->  ( abs `  ( A  -  Q ) )  =  ( abs `  ( C  -  Q ) ) )   &    |-  ( ph  ->  ( abs `  ( A  -  Q ) )  =  ( abs `  ( D  -  Q ) ) )   =>    |-  ( ph  ->  (
 ( abs `  ( P  -  A ) )  x.  ( abs `  ( P  -  B ) ) )  =  ( ( abs `  ( P  -  C ) )  x.  ( abs `  ( P  -  D ) ) ) )
 
28-Feb-2017chordthmlem5 19877 If P is on the segment AB and AQ = BQ, then PA  x. PB = BQ2  - PQ2. This follows from two uses of chordthmlem3 19875 to show that PQ2 = QM2  + PM2 and BQ2 = QM2  + BM2, so BQ2  - PQ2 = (QM2  + BM2)  - (QM2  + PM2) = BM2  - PM2, which equals PA  x. PB by chordthmlem4 19876. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  Q  e.  CC )   &    |-  ( ph  ->  X  e.  ( 0 [,] 1
 ) )   &    |-  ( ph  ->  P  =  ( ( X  x.  A )  +  ( ( 1  -  X )  x.  B ) ) )   &    |-  ( ph  ->  ( abs `  ( A  -  Q ) )  =  ( abs `  ( B  -  Q ) ) )   =>    |-  ( ph  ->  (
 ( abs `  ( P  -  A ) )  x.  ( abs `  ( P  -  B ) ) )  =  ( ( ( abs `  ( B  -  Q ) ) ^ 2 )  -  ( ( abs `  ( P  -  Q ) ) ^ 2 ) ) )
 
28-Feb-2017chordthmlem4 19876 If P is on the segment AB and M is the midpoint of AB, then PA  x. PB = BM2  - PM2. If all lengths are reexpressed as fractions of AB, this reduces to the identity  X  x.  (
1  -  X )  =  ( 1  / 
2 )2  -  ( ( 1  /  2 )  -  X )2. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  X  e.  (
 0 [,] 1 ) )   &    |-  ( ph  ->  M  =  ( ( A  +  B )  /  2
 ) )   &    |-  ( ph  ->  P  =  ( ( X  x.  A )  +  ( ( 1  -  X )  x.  B ) ) )   =>    |-  ( ph  ->  ( ( abs `  ( P  -  A ) )  x.  ( abs `  ( P  -  B ) ) )  =  ( ( ( abs `  ( B  -  M ) ) ^ 2 )  -  ( ( abs `  ( P  -  M ) ) ^ 2 ) ) )
 
28-Feb-2017chordthmlem3 19875 If M is the midpoint of AB, AQ = BQ, and P is on the line AB, then PQ2 = QM2  + PM2. This follows from chordthmlem2 19874 and the Pythagorean theorem (pythag 19859) in the case where P and Q are unequal to M. If either P or Q equals M, the result is trivial. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  Q  e.  CC )   &    |-  ( ph  ->  X  e.  RR )   &    |-  ( ph  ->  M  =  ( ( A  +  B )  / 
 2 ) )   &    |-  ( ph  ->  P  =  ( ( X  x.  A )  +  ( (
 1  -  X )  x.  B ) ) )   &    |-  ( ph  ->  ( abs `  ( A  -  Q ) )  =  ( abs `  ( B  -  Q ) ) )   =>    |-  ( ph  ->  (
 ( abs `  ( P  -  Q ) ) ^
 2 )  =  ( ( ( abs `  ( Q  -  M ) ) ^ 2 )  +  ( ( abs `  ( P  -  M ) ) ^ 2 ) ) )
 
28-Feb-2017chordthmlem2 19874 If M is the midpoint of AB, AQ = BQ, and P is on the line AB, then QMP is a right angle. This is proven by reduction to the special case chordthmlem 19873, where P = B, and using angrtmuld 19850 to observe that QMP is right iff QMB is. (Contributed by David Moews, 28-Feb-2017.)
 |-  F  =  ( x  e.  ( CC  \  { 0 } ) ,  y  e.  ( CC  \  { 0 } )  |->  ( Im `  ( log `  ( y  /  x ) ) ) )   &    |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  Q  e.  CC )   &    |-  ( ph  ->  X  e.  RR )   &    |-  ( ph  ->  M  =  ( ( A  +  B )  /  2 ) )   &    |-  ( ph  ->  P  =  ( ( X  x.  A )  +  (
 ( 1  -  X )  x.  B ) ) )   &    |-  ( ph  ->  ( abs `  ( A  -  Q ) )  =  ( abs `  ( B  -  Q ) ) )   &    |-  ( ph  ->  P  =/=  M )   &    |-  ( ph  ->  Q  =/=  M )   =>    |-  ( ph  ->  (
 ( Q  -  M ) F ( P  -  M ) )  e. 
 { ( pi  / 
 2 ) ,  -u ( pi  /  2 ) }
 )
 
28-Feb-2017chordthmlem 19873 If M is the midpoint of AB and AQ = BQ, then QMB is a right angle. The proof uses ssscongptld 19866 to observe that, since AMQ and BMQ have equal sides, the angles QMB and QMA must be equal. Since they are supplementary, both must be right. (Contributed by David Moews, 28-Feb-2017.)
 |-  F  =  ( x  e.  ( CC  \  { 0 } ) ,  y  e.  ( CC  \  { 0 } )  |->  ( Im `  ( log `  ( y  /  x ) ) ) )   &    |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  Q  e.  CC )   &    |-  ( ph  ->  M  =  ( ( A  +  B )  / 
 2 ) )   &    |-  ( ph  ->  ( abs `  ( A  -  Q ) )  =  ( abs `  ( B  -  Q ) ) )   &    |-  ( ph  ->  A  =/=  B )   &    |-  ( ph  ->  Q  =/=  M )   =>    |-  ( ph  ->  (
 ( Q  -  M ) F ( B  -  M ) )  e. 
 { ( pi  / 
 2 ) ,  -u ( pi  /  2 ) }
 )
 
28-Feb-2017angpieqvd 19872 The angle ABC is  pi iff B is a nontrivial convex combination of A and C, i.e., iff B is in the interior of the segment AC. (Contributed by David Moews, 28-Feb-2017.)
 |-  F  =  ( x  e.  ( CC  \  { 0 } ) ,  y  e.  ( CC  \  { 0 } )  |->  ( Im `  ( log `  ( y  /  x ) ) ) )   &    |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  A  =/=  B )   &    |-  ( ph  ->  B  =/=  C )   =>    |-  ( ph  ->  (
 ( ( A  -  B ) F ( C  -  B ) )  =  pi  <->  E. w  e.  (
 0 (,) 1 ) B  =  ( ( w  x.  A )  +  ( ( 1  -  w )  x.  C ) ) ) )
 
28-Feb-2017angpined 19871 If the angle at ABC is  pi, then A is not equal to C. (Contributed by David Moews, 28-Feb-2017.)
 |-  F  =  ( x  e.  ( CC  \  { 0 } ) ,  y  e.  ( CC  \  { 0 } )  |->  ( Im `  ( log `  ( y  /  x ) ) ) )   &    |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  A  =/=  B )   &    |-  ( ph  ->  B  =/=  C )   =>    |-  ( ph  ->  (
 ( ( A  -  B ) F ( C  -  B ) )  =  pi  ->  A  =/=  C ) )
 
28-Feb-2017angpieqvdlem2 19870 Equivalence used in angpieqvd 19872. (Contributed by David Moews, 28-Feb-2017.)
 |-  F  =  ( x  e.  ( CC  \  { 0 } ) ,  y  e.  ( CC  \  { 0 } )  |->  ( Im `  ( log `  ( y  /  x ) ) ) )   &    |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  A  =/=  B )   &    |-  ( ph  ->  B  =/=  C )   =>    |-  ( ph  ->  ( -u ( ( C  -  B )  /  ( A  -  B ) )  e.  RR+  <->  ( ( A  -  B ) F ( C  -  B ) )  =  pi ) )
 
28-Feb-2017angpieqvdlem 19869 Equivalence used in the proof of angpieqvd 19872. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  A  =/=  B )   &    |-  ( ph  ->  A  =/=  C )   =>    |-  ( ph  ->  (
 -u ( ( C  -  B )  /  ( A  -  B ) )  e.  RR+  <->  ( ( C  -  B )  /  ( C  -  A ) )  e.  (
 0 (,) 1 ) ) )
 
28-Feb-2017affineequiv2 19868 Equivalence between two ways of expressing  B as an affine combination of  A and  C. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  D  e.  CC )   =>    |-  ( ph  ->  ( B  =  ( ( D  x.  A )  +  ( ( 1  -  D )  x.  C ) )  <->  ( B  -  A )  =  (
 ( 1  -  D )  x.  ( C  -  A ) ) ) )
 
28-Feb-2017affineequiv 19867 Equivalence between two ways of expressing  B as an affine combination of  A and  C. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  D  e.  CC )   =>    |-  ( ph  ->  ( B  =  ( ( D  x.  A )  +  ( ( 1  -  D )  x.  C ) )  <->  ( C  -  B )  =  ( D  x.  ( C  -  A ) ) ) )
 
28-Feb-2017ssscongptld 19866 If two triangles have equal sides, one angle in one triangle has the same cosine as the corresponding angle in the other triangle. This is a partial form of the SSS congruence theorem.

This theorem is proven by using lawcos 19858 on both triangles to express one side in terms of the other two, and then equating these expressions and reducing this algebraically to get an equality of cosines of angles. (Contributed by David Moews, 28-Feb-2017.)

 |-  F  =  ( x  e.  ( CC  \  { 0 } ) ,  y  e.  ( CC  \  { 0 } )  |->  ( Im `  ( log `  ( y  /  x ) ) ) )   &    |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  D  e.  CC )   &    |-  ( ph  ->  E  e.  CC )   &    |-  ( ph  ->  G  e.  CC )   &    |-  ( ph  ->  A  =/=  B )   &    |-  ( ph  ->  B  =/=  C )   &    |-  ( ph  ->  D  =/=  E )   &    |-  ( ph  ->  E  =/=  G )   &    |-  ( ph  ->  ( abs `  ( A  -  B ) )  =  ( abs `  ( D  -  E ) ) )   &    |-  ( ph  ->  ( abs `  ( B  -  C ) )  =  ( abs `  ( E  -  G ) ) )   &    |-  ( ph  ->  ( abs `  ( C  -  A ) )  =  ( abs `  ( G  -  D ) ) )   =>    |-  ( ph  ->  ( cos `  ( ( A  -  B ) F ( C  -  B ) ) )  =  ( cos `  (
 ( D  -  E ) F ( G  -  E ) ) ) )
 
28-Feb-2017angrtmuld 19850 Perpendicularity of two vectors does not change under rescaling the second. (Contributed by David Moews, 28-Feb-2017.)
 |-  F  =  ( x  e.  ( CC  \  { 0 } ) ,  y  e.  ( CC  \  { 0 } )  |->  ( Im `  ( log `  ( y  /  x ) ) ) )   &    |-  ( ph  ->  X  e.  CC )   &    |-  ( ph  ->  Y  e.  CC )   &    |-  ( ph  ->  Z  e.  CC )   &    |-  ( ph  ->  X  =/=  0 )   &    |-  ( ph  ->  Y  =/=  0
 )   &    |-  ( ph  ->  Z  =/=  0 )   &    |-  ( ph  ->  ( Z  /  Y )  e.  RR )   =>    |-  ( ph  ->  ( ( X F Y )  e.  { ( pi  /  2 ) ,  -u ( pi  /  2
 ) }  <->  ( X F Z )  e.  { ( pi  /  2 ) ,  -u ( pi  /  2
 ) } ) )
 
28-Feb-2017cosangneg2d 19849 The cosine of the angle between  X and  -u Y is the negative of that between  X and  Y. If A, B and C are collinear points, this implies that the cosines of DBA and DBC sum to zero, i.e., that DBA and DBC are supplementary. (Contributed by David Moews, 28-Feb-2017.)
 |-  F  =  ( x  e.  ( CC  \  { 0 } ) ,  y  e.  ( CC  \  { 0 } )  |->  ( Im `  ( log `  ( y  /  x ) ) ) )   &    |-  ( ph  ->  X  e.  CC )   &    |-  ( ph  ->  X  =/=  0
 )   &    |-  ( ph  ->  Y  e.  CC )   &    |-  ( ph  ->  Y  =/=  0 )   =>    |-  ( ph  ->  ( cos `  ( X F -u Y ) )  =  -u ( cos `  ( X F Y ) ) )
 
28-Feb-2017angrteqvd 19848 Two vectors are at a right angle iff their quotient is purely imaginary. (Contributed by David Moews, 28-Feb-2017.)
 |-  F  =  ( x  e.  ( CC  \  { 0 } ) ,  y  e.  ( CC  \  { 0 } )  |->  ( Im `  ( log `  ( y  /  x ) ) ) )   &    |-  ( ph  ->  X  e.  CC )   &    |-  ( ph  ->  X  =/=  0
 )   &    |-  ( ph  ->  Y  e.  CC )   &    |-  ( ph  ->  Y  =/=  0 )   =>    |-  ( ph  ->  ( ( X F Y )  e.  { ( pi  /  2 ) ,  -u ( pi  /  2
 ) }  <->  ( Re `  ( Y  /  X ) )  =  0 ) )
 
28-Feb-2017angcld 19847 The (signed) angle between two vectors is in  (
-u pi (,] pi ). Deduction form. (Contributed by David Moews, 28-Feb-2017.)
 |-  F  =  ( x  e.  ( CC  \  { 0 } ) ,  y  e.  ( CC  \  { 0 } )  |->  ( Im `  ( log `  ( y  /  x ) ) ) )   &    |-  ( ph  ->  X  e.  CC )   &    |-  ( ph  ->  X  =/=  0
 )   &    |-  ( ph  ->  Y  e.  CC )   &    |-  ( ph  ->  Y  =/=  0 )   =>    |-  ( ph  ->  ( X F Y )  e.  ( -u pi (,] pi ) )
 
28-Feb-2017angvald 19846 The (signed) angle between two vectors is the argument of their quotient. Deduction form of angval 19843. (Contributed by David Moews, 28-Feb-2017.)
 |-  F  =  ( x  e.  ( CC  \  { 0 } ) ,  y  e.  ( CC  \  { 0 } )  |->  ( Im `  ( log `  ( y  /  x ) ) ) )   &    |-  ( ph  ->  X  e.  CC )   &    |-  ( ph  ->  X  =/=  0
 )   &    |-  ( ph  ->  Y  e.  CC )   &    |-  ( ph  ->  Y  =/=  0 )   =>    |-  ( ph  ->  ( X F Y )  =  ( Im `  ( log `  ( Y  /  X ) ) ) )
 
28-Feb-2017cosarg0d 19795 The cosine of the argument is zero precisely on the imaginary axis. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  X  e.  CC )   &    |-  ( ph  ->  X  =/=  0 )   =>    |-  ( ph  ->  ( ( cos `  ( Im `  ( log `  X ) ) )  =  0  <->  ( Re `  X )  =  0
 ) )
 
28-Feb-2017cosargd 19794 The cosine of the argument is the quotient of the real part and the absolute value. Compare to efiarg 19793. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  X  e.  CC )   &    |-  ( ph  ->  X  =/=  0 )   =>    |-  ( ph  ->  ( cos `  ( Im `  ( log `  X ) ) )  =  ( ( Re `  X )  /  ( abs `  X ) ) )
 
28-Feb-2017logimclad 19762 The imaginary part of the logarithm is in  ( -u pi (,] pi ). Alternate form of logimcld 19761. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  X  e.  CC )   &    |-  ( ph  ->  X  =/=  0 )   =>    |-  ( ph  ->  ( Im `  ( log `  X ) )  e.  ( -u pi (,] pi ) )
 
28-Feb-2017logimcld 19761 The imaginary part of the logarithm is in  ( -u pi (,] pi ). Deduction form of logimcl 19759. Compare logimclad 19762. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  X  e.  CC )   &    |-  ( ph  ->  X  =/=  0 )   =>    |-  ( ph  ->  (
 -u pi  <  ( Im `  ( log `  X ) )  /\  ( Im
 `  ( log `  X ) )  <_  pi ) )
 
28-Feb-2017logcld 19760 The logarithm of a nonzero complex number is a complex number. Deduction form of logcl 19758. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  X  e.  CC )   &    |-  ( ph  ->  X  =/=  0 )   =>    |-  ( ph  ->  ( log `  X )  e.  CC )
 
28-Feb-2017negpitopissre 19734  ( -u pi (,] pi ) is a subset of the reals. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( -u pi (,] pi )  C_  RR
 
28-Feb-2017coseq0negpitopi 19703 Location of the zeroes of cosine in 
( -u pi (,] pi ). (Contributed by David Moews, 28-Feb-2017.)
 |-  ( A  e.  ( -u pi (,] pi ) 
 ->  ( ( cos `  A )  =  0  <->  A  e.  { ( pi  /  2 ) ,  -u ( pi  /  2
 ) } ) )
 
28-Feb-2017coseq00topi 19702 Location of the zeroes of cosine in 
( 0 [,] pi ). (Contributed by David Moews, 28-Feb-2017.)
 |-  ( A  e.  (
 0 [,] pi )  ->  ( ( cos `  A )  =  0  <->  A  =  ( pi  /  2 ) ) )
 
28-Feb-2017cosneghalfpi 19670 The cosine of  -u pi  /  2 is zero. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( cos `  -u ( pi  /  2 ) )  =  0
 
28-Feb-2017halfpire 19667  pi  /  2 is real. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( pi  /  2
 )  e.  RR
 
28-Feb-2017abs00bd 11653 If a complex number is zero, its absolute value is zero. Converse of abs00d 11805. One-way deduction form of abs00 11651. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  =  0 )   =>    |-  ( ph  ->  ( abs `  A )  =  0 )
 
28-Feb-2017abs00ad 11652 A complex number is zero iff its absolute value is zero. Deduction form of abs00 11651. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   =>    |-  ( ph  ->  (
 ( abs `  A )  =  0  <->  A  =  0
 ) )
 
28-Feb-2017sq0id 11075 If a number is zero, its square is zero. Deduction form of sq0i 11074. Converse of sqeq0d 11122. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  =  0 )   =>    |-  ( ph  ->  ( A ^ 2 )  =  0 )
 
28-Feb-2017unitssre 10659  ( 0 [,] 1 ) is a subset of the reals. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( 0 [,] 1
 )  C_  RR
 
28-Feb-2017xov1plusxeqvd 10658 A complex number  X is positive real iff  X  /  (
1  +  X ) is in  ( 0 (,) 1 ). Deduction form. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  X  e.  CC )   &    |-  ( ph  ->  X  =/=  -u 1 )   =>    |-  ( ph  ->  ( X  e.  RR+  <->  ( X  /  ( 1  +  X ) )  e.  (
 0 (,) 1 ) ) )
 
28-Feb-2017rehalfcli 9839 Half a real number is real. Inference form. (Contributed by David Moews, 28-Feb-2017.)
 |-  A  e.  RR   =>    |-  ( A  / 
 2 )  e.  RR
 
28-Feb-2017div2subd 9466 Swap subtrahend and minuend inside the numerator and denominator of a fraction. Deduction form of div2sub 9465. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  D  e.  CC )   &    |-  ( ph  ->  C  =/=  D )   =>    |-  ( ph  ->  ( ( A  -  B )  /  ( C  -  D ) )  =  ( ( B  -  A )  /  ( D  -  C ) ) )
 
28-Feb-2017diveq1bd 9464 If two complex numbers are equal, their quotient is one. One-way deduction form of diveq1 9334. Converse of diveq1d 9424. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  B  =/=  0 )   &    |-  ( ph  ->  A  =  B )   =>    |-  ( ph  ->  ( A  /  B )  =  1 )
 
28-Feb-2017dmdcan2d 9446 Cancellation law for division and multiplication. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  B  =/=  0 )   &    |-  ( ph  ->  C  =/=  0 )   =>    |-  ( ph  ->  ( ( A  /  B )  x.  ( B  /  C ) )  =  ( A  /  C ) )
 
28-Feb-2017divne1d 9427 If two complex numbers are unequal, their quotient is not one. Contrapositive of diveq1d 9424. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  B  =/=  0
 )   &    |-  ( ph  ->  A  =/=  B )   =>    |-  ( ph  ->  ( A  /  B )  =/=  1 )
 
28-Feb-2017diveq0ad 9426 A fraction of complex numbers is zero iff its numerator is. Deduction form of diveq0 9314. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  B  =/=  0
 )   =>    |-  ( ph  ->  (
 ( A  /  B )  =  0  <->  A  =  0
 ) )
 
28-Feb-2017diveq1ad 9425 The quotient of two complex numbers is one iff they are equal. Deduction form of diveq1 9334. Generalization of diveq1d 9424. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  B  =/=  0
 )   =>    |-  ( ph  ->  (
 ( A  /  B )  =  1  <->  A  =  B ) )
 
28-Feb-2017eqnegad 9362 If a complex number equals its own negative, it is zero. One-way deduction form of eqneg 9360. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  A  =  -u A )   =>    |-  ( ph  ->  A  =  0 )
 
28-Feb-2017eqnegd 9361 A complex number equals its negative iff it is zero. Deduction form of eqneg 9360. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   =>    |-  ( ph  ->  ( A  =  -u A  <->  A  =  0
 ) )
 
28-Feb-2017mulne0bbd 9302 A factor of a nonzero complex number is nonzero. Partial converse of mulne0d 9300 and consequence of mulne0bd 9299. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  ( A  x.  B )  =/=  0
 )   =>    |-  ( ph  ->  B  =/=  0 )
 
28-Feb-2017mulne0bad 9301 A factor of a nonzero complex number is nonzero. Partial converse of mulne0d 9300 and consequence of mulne0bd 9299. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  ( A  x.  B )  =/=  0
 )   =>    |-  ( ph  ->  A  =/=  0 )
 
28-Feb-2017mulcan2ad 9284 Cancellation of a nonzero factor on the right in an equation. One-way deduction form of mulcan2d 9282. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  C  =/=  0 )   &    |-  ( ph  ->  ( A  x.  C )  =  ( B  x.  C ) )   =>    |-  ( ph  ->  A  =  B )
 
28-Feb-2017mulcanad 9283 Cancellation of a nonzero factor on the left in an equation. One-way deduction form of mulcand 9281. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  C  =/=  0 )   &    |-  ( ph  ->  ( C  x.  A )  =  ( C  x.  B ) )   =>    |-  ( ph  ->  A  =  B )
 
28-Feb-2017lt0ne0d 9218 Something less than zero is not zero. Deduction form. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  <  0 )   =>    |-  ( ph  ->  A  =/=  0 )
 
28-Feb-2017subeq0bd 9089 If two complex numbers are equal, their difference is zero. Consequence of subeq0ad 9047. Converse of subeq0d 9045. Contrapositive of subne0ad 9048. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  A  =  B )   =>    |-  ( ph  ->  ( A  -  B )  =  0 )
 
28-Feb-2017subneintr2d 9083 Introducing subtraction on both sides of a statement of nonequality. Contrapositive of subcan2d 9079. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  A  =/=  B )   =>    |-  ( ph  ->  ( A  -  C )  =/=  ( B  -  C ) )
 
28-Feb-2017subcan2ad 9082 Cancellation law for subtraction. Deduction form of subcan2 8952. Generalization of subcan2d 9079. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   =>    |-  ( ph  ->  (
 ( A  -  C )  =  ( B  -  C )  <->  A  =  B ) )
 
28-Feb-2017subneintrd 9081 Introducing subtraction on both sides of a statement of nonequality. Contrapositive of subcand 9078. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  B  =/=  C )   =>    |-  ( ph  ->  ( A  -  B )  =/=  ( A  -  C ) )
 
28-Feb-2017subcanad 9080 Cancellation law for subtraction. Deduction form of subcan 8982. Generalization of subcand 9078. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   =>    |-  ( ph  ->  (
 ( A  -  B )  =  ( A  -  C )  <->  B  =  C ) )
 
28-Feb-2017subne0ad 9048 If the difference of two complex numbers is nonzero, they are unequal. Converse of subne0d 9046. Contrapositive of subeq0bd 9089. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  ( A  -  B )  =/=  0
 )   =>    |-  ( ph  ->  A  =/=  B )
 
28-Feb-2017subeq0ad 9047 The difference of two complex numbers is zero iff they are equal. Deduction form of subeq0 8953. Generalization of subeq0d 9045. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   =>    |-  ( ph  ->  ( ( A  -  B )  =  0  <->  A  =  B ) )
 
28-Feb-2017negned 9034 If two complex numbers are unequal, so are their negatives. Contrapositive of neg11d 9049. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  A  =/=  B )   =>    |-  ( ph  ->  -u A  =/=  -u B )
 
28-Feb-2017neg11ad 9033 The negatives of two complex numbers are equal iff they are equal. Deduction form of neg11 8978. Generalization of neg11d 9049. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   =>    |-  ( ph  ->  (
 -u A  =  -u B 
 <->  A  =  B ) )
 
28-Feb-2017negcon1ad 9032 Contraposition law for unary minus. One-way deduction form of negcon1 8979. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  -u A  =  B )   =>    |-  ( ph  ->  -u B  =  A )
 
28-Feb-2017negcon1d 9031 Contraposition law for unary minus. Deduction form of negcon1 8979. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   =>    |-  ( ph  ->  (
 -u A  =  B  <->  -u B  =  A )
 )
 
28-Feb-2017addneintr2d 8900 Introducing a term on the right-hand side of a sum in a negated equality. Contrapositive of addcan2ad 8898. Consequence of addcan2d 8896. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  A  =/=  B )   =>    |-  ( ph  ->  ( A  +  C )  =/=  ( B  +  C ) )
 
28-Feb-2017addneintrd 8899 Introducing a term on the left-hand side of a sum in a negated equality. Contrapositive of addcanad 8897. Consequence of addcand 8895. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  B  =/=  C )   =>    |-  ( ph  ->  ( A  +  B )  =/=  ( A  +  C ) )
 
28-Feb-2017addcan2ad 8898 Cancelling a term on the right-hand side of a sum in an equality. Consequence of addcan2d 8896. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  ( A  +  C )  =  ( B  +  C ) )   =>    |-  ( ph  ->  A  =  B )
 
28-Feb-2017addcanad 8897 Cancelling a term on the left-hand side of a sum in an equality. Consequence of addcand 8895. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  ( A  +  B )  =  ( A  +  C ) )   =>    |-  ( ph  ->  B  =  C )
 
28-Feb-2017rexri 8764 A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.)
 |-  A  e.  RR   =>    |-  A  e.  RR*
 
28-Feb-2017pm2.21ddne 2486 A contradiction implies anything. Equality/inequality deduction form. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  A  =/=  B )   =>    |-  ( ph  ->  ps )
 
28-Feb-2017neneqad 2482 If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2428. One-way deduction form of df-ne 2414. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  -.  A  =  B )   =>    |-  ( ph  ->  A  =/=  B )
 
19-Feb-2017ex-natded9.20-2 20663 A more efficient proof of Theorem 9.20 of [Laboreo] p. 45. Compare with ex-natded9.20 20662. (Proof modification is discouraged.) (Contributed by David A. Wheeler, 19-Feb-2017.)
 |-  ( ph  ->  ( ps  /\  ( ch  \/  th ) ) )   =>    |-  ( ph  ->  ( ( ps  /\  ch )  \/  ( ps  /\  th ) ) )
 
19-Feb-2017ex-natded9.20 20662 Theorem 9.20 of [Laboreo] p. 43, translated line by line using the usual translation of natural deduction (ND) in the Metamath Proof Explorer (MPE) notation. For information about ND and Metamath, see the page on Deduction Form and Natural Deduction in Metamath Proof Explorer. The original proof, which uses Fitch style, was written as follows (the leading "..." shows an embedded ND hypothesis, beginning with the initial assumption of the ND hypothesis):
#MPE#ND Expression MPE TranslationND Rationale MPE Rationale
11  ( ps  /\  ( ch  \/  th ) )  ( ph  ->  ( ps  /\  ( ch  \/  th ) ) ) Given $e
22  ps  ( ph  ->  ps )  /\EL 1 simpld 447 1
311  ( ch  \/  th )  ( ph  ->  ( ch  \/  th ) )  /\ER 1 simprd 451 1
44 ...|  ch  ( ( ph  /\  ch )  ->  ch ) ND hypothesis assumption simpr 449
55 ...  ( ps  /\  ch )  ( ( ph  /\  ch )  ->  ( ps  /\  ch ) )  /\I 2,4 jca 520 3,4
66 ...  ( ( ps  /\  ch )  \/  ( ps  /\  th ) )  ( ( ph  /\  ch )  ->  ( ( ps  /\  ch )  \/  ( ps  /\  th ) ) )  \/IR 5 orcd 383 5
78 ...|  th  ( ( ph  /\  th )  ->  th ) ND hypothesis assumption simpr 449
89 ...  ( ps  /\  th )  ( ( ph  /\  th )  ->  ( ps  /\  th ) )  /\I 2,7 jca 520 7,8
910 ...  ( ( ps  /\  ch )  \/  ( ps  /\  th ) )  ( ( ph  /\  th )  ->  ( ( ps  /\  ch )  \/  ( ps  /\  th ) ) )  \/IL 8 olcd 384 9
1012  ( ( ps  /\  ch )  \/  ( ps  /\  th ) )  ( ph  ->  ( ( ps  /\  ch )  \/  ( ps  /\  th ) ) )  \/E 3,6,9 mpjaodan 764 6,10,11

The original used Latin letters; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including  ph and uses the Metamath equivalents of the natural deduction rules. To add an assumption, the antecedent is modified to include it (typically by using adantr 453; simpr 449 is useful when you want to depend directly on the new assumption). Below is the final metamath proof (which reorders some steps).

A much more efficient proof is ex-natded9.20-2 20663. (Proof modification is discouraged.) (Contributed by David A. Wheeler, 19-Feb-2017.)

 |-  ( ph  ->  ( ps  /\  ( ch  \/  th ) ) )   =>    |-  ( ph  ->  ( ( ps  /\  ch )  \/  ( ps  /\  th ) ) )
 
19-Feb-2017ex-natded5.5 20655 Theorem 5.5 of [Laboreo] p. 18, translated line by line using the usual translation of natural deduction (ND) in the Metamath Proof Explorer (MPE) notation. For information about ND and Metamath, see the page on Deduction Form and Natural Deduction in Metamath Proof Explorer. The original proof, which uses Fitch style, was written as follows (the leading "..." shows an embedded ND hypothesis, beginning with the initial assumption of the ND hypothesis):
#MPE#ND Expression MPE TranslationND Rationale MPE Rationale
12;3  ( ps  ->  ch )  ( ph  ->  ( ps  ->  ch ) ) Given $e; adantr 453 to move it into the ND hypothesis
25  -.  ch  ( ph  ->  -.  ch ) Given $e; we'll use adantr 453 to move it into the ND hypothesis
31 ...|  ps  ( ph  ->  ps ) ND hypothesis assumption simpr 449
44 ...  ch  ( ( ph  /\  ps )  ->  ch )  ->E 1,3 mpd 16 1,3
56 ...  -.  ch  ( ( ph  /\  ps )  ->  -.  ch ) IT 2 adantr 453 5
67  -.  ps  ( ph  ->  -.  ps )  /\I 3,4,5 pm2.65da 562 4,6

The original used Latin letters; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including  ph and uses the Metamath equivalents of the natural deduction rules. To add an assumption, the antecedent is modified to include it (typically by using adantr 453; simpr 449 is useful when you want to depend directly on the new assumption). Below is the final metamath proof (which reorders some steps).

A much more efficient proof is mtod 170; a proof without context is shown in mto 169.

(Proof modification is discouraged.) (Contributed by David A. Wheeler, 19-Feb-2017.)

 |-  ( ph  ->  ( ps  ->  ch ) )   &    |-  ( ph  ->  -.  ch )   =>    |-  ( ph  ->  -.  ps )
 
18-Feb-2017sbidd-misc 26878 An identity theorem for substitution. See sbid 1895. See Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint). (Contributed by DAW, 18-Feb-2017.)
 |-  (
 ( ph  ->  [ x  /  x ] ps )  <->  (
 ph  ->  ps ) )
 
18-Feb-2017sbidd 26877 An identity theorem for substitution. See sbid 1895. See Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint). (Contributed by DAW, 18-Feb-2017.)
 |-  ( ph  ->  [ x  /  x ] ps )   =>    |-  ( ph  ->  ps )
 
18-Feb-2017ex-natded9.26 20664 Theorem 9.26 of [Laboreo] p. 45, translated line by line using an interpretation of natural deduction in Metamath. This proof has some additional complications due to the fact that Metamath's existential elimination rule does not change bound variables, so we need to verify that  x is bound in the conclusion. For information about ND and Metamath, see the page on Deduction Form and Natural Deduction in Metamath Proof Explorer. The original proof, which uses Fitch style, was written as follows (the leading "..." shows an embedded ND hypothesis, beginning with the initial assumption of the ND hypothesis):
#MPE#ND Expression MPE TranslationND Rationale MPE Rationale
13  E. x A. y ps ( x ,  y )  ( ph  ->  E. x A. y ps ) Given $e.
26 ...|  A. y ps ( x ,  y )  ( ( ph  /\  A. y ps )  ->  A. y ps ) ND hypothesis assumption simpr 449. Later statements will have this scope.
37;5,4 ...  ps ( x ,  y )  ( ( ph  /\  A. y ps )  ->  ps )  A.E 2,y a4sbcd 2934 ( A.E), 5,6. To use it we need a1i 12 and vex 2730. This could be immediately done with 19.21bi 1774, but we want to show the general approach for substitution.
412;8,9,10,11 ...  E. x ps ( x ,  y )  ( ( ph  /\  A. y ps )  ->  E. x ps )  E.I 3,a a4esbcd 3003 ( E.I), 11. To use it we need sylibr 205, which in turn requires sylib 190 and two uses of sbcid 2937. This could be more immediately done using 19.8a 1758, but we want to show the general approach for substitution.
513;1,2  E. x ps ( x ,  y )  ( ph  ->  E. x ps )  E.E 1,2,4,a exlimdd 1933 ( E.E), 1,2,3,12. We'll need supporting assertions that the variable is free (not bound), as provided in nfv 1629 and nfe1 1566 (MPE# 1,2)
614  A. y E. x ps ( x ,  y )  ( ph  ->  A. y E. x ps )  A.I 5 alrimiv 2012 ( A.I), 13

The original used Latin letters for predicates; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including  ph and uses the Metamath equivalents of the natural deduction rules. Below is the final metamath proof (which reorders some steps).

Note that in the original proof,  ps ( x ,  y ) has explicit parameters. In Metamath, these parameters are always implicit, and the parameters upon which a wff variable can depend are recorded in the "allowed substitution hints" below.

A much more efficient proof, using more of Metamath and MPE's capabilities, is shown in ex-natded9.26-2 20665.

(Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.) (Revised by David A. Wheeler, 18-Feb-2017.)

 |-  ( ph  ->  E. x A. y ps )   =>    |-  ( ph  ->  A. y E. x ps )
 
18-Feb-2017sbcid 2937 An identity theorem for substitution. See sbid 1895. (Contributed by Mario Carneiro, 18-Feb-2017.)
 |-  ( [. x  /  x ]. ph  <->  ph )
 
13-Feb-201719.8ad 26876 If a wff is true, it is true for at least one instance. Deductive form of 19.8a 1758. (Contributed by DAW, 13-Feb-2017.)
 |-  ( ph  ->  ps )   =>    |-  ( ph  ->  E. x ps )
 
9-Feb-2017resolution 26954 Resolution rule. This is the primary inference rule in some automated theorem provers such as prover9. The resolution rule can be traced back to Davis and Putnam (1960). (Contributed by David A. Wheeler, 9-Feb-2017.)
 |-  (
 ( ( ph  /\  ps )  \/  ( -.  ph  /\ 
 ch ) )  ->  ( ps  \/  ch )
 )
 
9-Feb-2017ex-natded9.26-2 20665 A more efficient proof of Theorem 9.26 of [Laboreo] p. 45. Compare with ex-natded9.26 20664. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ph  ->  E. x A. y ps )   =>    |-  ( ph  ->  A. y E. x ps )
 
9-Feb-2017ex-natded5.13-2 20661 A more efficient proof of Theorem 5.13 of [Laboreo] p. 20. Compare with ex-natded5.13 20660. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ph  ->  ( ps  \/  ch ) )   &    |-  ( ph  ->  ( ps  ->  th ) )   &    |-  ( ph  ->  ( -.  ta  ->  -.  ch ) )   =>    |-  ( ph  ->  ( th  \/  ta ) )
 
9-Feb-2017ex-natded5.13 20660 Theorem 5.13 of [Laboreo] p. 20, translated line by line using the interpretation of natural deduction in Metamath. For information about ND and Metamath, see the page on Deduction Form and Natural Deduction in Metamath Proof Explorer. A much more efficient proof, using more of Metamath and MPE's capabilities, is shown in ex-natded5.13-2 20661. The original proof, which uses Fitch style, was written as follows (the leading "..." shows an embedded ND hypothesis, beginning with the initial assumption of the ND hypothesis):
#MPE#ND Expression MPE TranslationND Rationale MPE Rationale
115  ( ps  \/  ch )  ( ph  ->  ( ps  \/  ch ) ) Given $e.
2;32  ( ps  ->  th )  ( ph  ->  ( ps  ->  th ) ) Given $e. adantr 453 to move it into the ND hypothesis
39  ( -.  ta  ->  -.  ch )  ( ph  ->  ( -.  ta  ->  -.  ch ) ) Given $e. ad2antrr 709 to move it into the ND sub-hypothesis
41 ...|  ps  ( ( ph  /\  ps )  ->  ps ) ND hypothesis assumption simpr 449
54 ...  th  ( ( ph  /\  ps )  ->  th )  ->E 2,4 mpd 16 1,3
65 ...  ( th  \/  ta )  ( ( ph  /\  ps )  ->  ( th  \/  ta ) )  \/I 5 orcd 383 4
76 ...|  ch  ( ( ph  /\  ch )  ->  ch ) ND hypothesis assumption simpr 449
88 ... ...|  -.  ta  ( ( ( ph  /\  ch )  /\  -.  ta )  ->  -.  ta ) (sub) ND hypothesis assumption simpr 449
911 ... ...  -.  ch  ( ( ( ph  /\  ch )  /\  -.  ta )  ->  -.  ch )  ->E 3,8 mpd 16 8,10
107 ... ...  ch  ( ( ( ph  /\  ch )  /\  -.  ta )  ->  ch ) IT 7 adantr 453 6
1112 ...  -.  -.  ta  ( ( ph  /\  ch )  ->  -.  -.  ta )  -.I 8,9,10 pm2.65da 562 7,11
1213 ...  ta  ( ( ph  /\  ch )  ->  ta )  -.E 11 notnotrd 107 12
1314 ...  ( th  \/  ta )  ( ( ph  /\  ch )  ->  ( th  \/  ta ) )  \/I 12 olcd 384 13
1416  ( th  \/  ta )  ( ph  ->  ( th  \/  ta ) )  \/E 1,6,13 mpjaodan 764 5,14,15

The original used Latin letters; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including  ph and uses the Metamath equivalents of the natural deduction rules. To add an assumption, the antecedent is modified to include it (typically by using adantr 453; simpr 449 is useful when you want to depend directly on the new assumption). (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.)

 |-  ( ph  ->  ( ps  \/  ch ) )   &    |-  ( ph  ->  ( ps  ->  th ) )   &    |-  ( ph  ->  ( -.  ta  ->  -.  ch ) )   =>    |-  ( ph  ->  ( th  \/  ta ) )
 
9-Feb-2017ex-natded5.8-2 20659 A more efficient proof of Theorem 5.8 of [Laboreo] p. 20. For a longer line-by-line translation, see ex-natded5.8 20658. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ph  ->  (
 ( ps  /\  ch )  ->  -.  th )
 )   &    |-  ( ph  ->  ( ta  ->  th ) )   &    |-  ( ph  ->  ch )   &    |-  ( ph  ->  ta )   =>    |-  ( ph  ->  -.  ps )
 
9-Feb-2017ex-natded5.8 20658 Theorem 5.8 of [Laboreo] p. 20, translated line by line using the usual translation of natural deduction (ND) in the Metamath Proof Explorer (MPE) notation. For information about ND and Metamath, see the page on Deduction Form and Natural Deduction in Metamath Proof Explorer. The original proof, which uses Fitch style, was written as follows (the leading "..." shows an embedded ND hypothesis, beginning with the initial assumption of the ND hypothesis):
#MPE#ND Expression MPE TranslationND Rationale MPE Rationale
110;11  ( ( ps  /\  ch )  ->  -.  th )  ( ph  ->  ( ( ps  /\  ch )  ->  -.  th ) ) Given $e; adantr 453 to move it into the ND hypothesis
23;4  ( ta  ->  th )  ( ph  ->  ( ta  ->  th ) ) Given $e; adantr 453 to move it into the ND hypothesis
37;8  ch  ( ph  ->  ch ) Given $e; adantr 453 to move it into the ND hypothesis
41;2  ta  ( ph  ->  ta ) Given $e. adantr 453 to move it into the ND hypothesis
56 ...|  ps  ( ( ph  /\  ps )  ->  ps ) ND Hypothesis/Assumption simpr 449. New ND hypothesis scope, each reference outside the scope must change antedent  ph to  ( ph  /\  ps ).
69 ...  ( ps  /\  ch )  ( ( ph  /\  ps )  ->  ( ps  /\  ch ) )  /\I 5,3 jca 520 ( /\I), 6,8 (adantr 453 to bring in scope)
75 ...  -.  th  ( ( ph  /\  ps )  ->  -.  th )  ->E 1,6 mpd 16 ( ->E), 2,4
812 ...  th  ( ( ph  /\  ps )  ->  th )  ->E 2,4 mpd 16 ( ->E), 9,11; note the contradiction with ND line 7 (MPE line 5)
913  -.  ps  ( ph  ->  -.  ps )  -.I 5,7,8 pm2.65da 562 ( -.I), 5,12; proof by contradiction. MPE step 6 (ND#5) does not need a reference here, because the assumption is embedded in the antecedents

The original used Latin letters; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including  ph and uses the Metamath equivalents of the natural deduction rules. To add an assumption, the antecedent is modified to include it (typically by using adantr 453; simpr 449 is useful when you want to depend directly on the new assumption). Below is the final metamath proof (which reorders some steps).

A much more efficient proof, using more of Metamath and MPE's capabilities, is shown in ex-natded5.8-2 20659.

(Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.)

 |-  ( ph  ->  (
 ( ps  /\  ch )  ->  -.  th )
 )   &    |-  ( ph  ->  ( ta  ->  th ) )   &    |-  ( ph  ->  ch )   &    |-  ( ph  ->  ta )   =>    |-  ( ph  ->  -.  ps )
 
9-Feb-2017ex-natded5.7-2 20657 A more efficient proof of Theorem 5.7 of [Laboreo] p. 19. Compare with ex-natded5.7 20656. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ph  ->  ( ps  \/  ( ch  /\  th ) ) )   =>    |-  ( ph  ->  ( ps  \/  ch )
 )
 
9-Feb-2017ex-natded5.7 20656 Theorem 5.7 of [Laboreo] p. 19, translated line by line using the interpretation of natural deduction in Metamath. A much more efficient proof, using more of Metamath and MPE's capabilities, is shown in ex-natded5.7-2 20657. For information about ND and Metamath, see the page on Deduction Form and Natural Deduction in Metamath Proof Explorer. The original proof, which uses Fitch style, was written as follows:

#MPE#ND Expression MPE TranslationND Rationale MPE Rationale
16  ( ps  \/  ( ch  /\  th ) )  ( ph  ->  ( ps  \/  ( ch  /\  th ) ) ) Given $e. No need for adantr 453 because we do not move this into an ND hypothesis
21 ...|  ps  ( ( ph  /\  ps )  ->  ps ) ND hypothesis assumption (new scope) simpr 449
32 ...  ( ps  \/  ch )  ( ( ph  /\  ps )  ->  ( ps  \/  ch ) )  \/IL 2 orcd 383, the MPE equivalent of  \/IL, 1
43 ...|  ( ch  /\  th )  ( ( ph  /\  ( ch  /\  th ) )  ->  ( ch  /\  th ) ) ND hypothesis assumption (new scope) simpr 449
54 ...  ch  ( ( ph  /\  ( ch  /\  th ) )  ->  ch )  /\EL 4 simpld 447, the MPE equivalent of  /\EL, 3
66 ...  ( ps  \/  ch )  ( ( ph  /\  ( ch  /\  th ) )  ->  ( ps  \/  ch ) )  \/IR 5 olcd 384, the MPE equivalent of  \/IR, 4
77  ( ps  \/  ch )  ( ph  ->  ( ps  \/  ch ) )  \/E 1,3,6 mpjaodan 764, the MPE equivalent of  \/E, 2,5,6

The original used Latin letters for predicates; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including  ph and uses the Metamath equivalents of the natural deduction rules. (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.)

 |-  ( ph  ->  ( ps  \/  ( ch  /\  th ) ) )   =>    |-  ( ph  ->  ( ps  \/  ch )
 )
 
9-Feb-2017ex-natded5.3i 20654 The same as ex-natded5.3 20652 and ex-natded5.3-2 20653 but with no context. (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ps  ->  ch )   &    |-  ( ch  ->  th )   =>    |-  ( ps  ->  ( ch  /\  th ) )
 
9-Feb-2017ex-natded5.3-2 20653 A more efficient proof of Theorem 5.3 of [Laboreo] p. 16. Compare with ex-natded5.3 20652 and ex-natded5.3i 20654. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ph  ->  ( ps  ->  ch ) )   &    |-  ( ph  ->  ( ch  ->  th ) )   =>    |-  ( ph  ->  ( ps  ->  ( ch  /\  th ) ) )
 
9-Feb-2017ex-natded5.3 20652 Theorem 5.3 of [Laboreo] p. 16, translated line by line using an interpretation of natural deduction in Metamath. A much more efficient proof, using more of Metamath and MPE's capabilities, is shown in ex-natded5.3-2 20653. A proof without context is shown in ex-natded5.3i 20654. For information about ND and Metamath, see the page on Deduction Form and Natural Deduction in Metamath Proof Explorer. The original proof, which uses Fitch style, was written as follows:

#MPE#ND Expression MPE TranslationND Rationale MPE Rationale
12;3  ( ps  ->  ch )  ( ph  ->  ( ps  ->  ch ) ) Given $e; adantr 453 to move it into the ND hypothesis
25;6  ( ch  ->  th )  ( ph  ->  ( ch  ->  th ) ) Given $e; adantr 453 to move it into the ND hypothesis
31 ...|  ps  ( ( ph  /\  ps )  ->  ps ) ND hypothesis assumption simpr 449, to access the new assumption
44 ...  ch  ( ( ph  /\  ps )  ->  ch )  ->E 1,3 mpd 16, the MPE equivalent of  ->E, 1.3. adantr 453 was used to transform its dependency (we could also use imp 420 to get this directly from 1)
57 ...  th  ( ( ph  /\  ps )  ->  th )  ->E 2,4 mpd 16, the MPE equivalent of  ->E, 4,6. adantr 453 was used to transform its dependency
68 ...  ( ch  /\  th )  ( ( ph  /\  ps )  ->  ( ch  /\  th ) )  /\I 4,5 jca 520, the MPE equivalent of  /\I, 4,7
79  ( ps  ->  ( ch  /\  th ) )  ( ph  ->  ( ps  ->  ( ch  /\  th ) ) )  ->I 3,6 ex 425, the MPE equivalent of  ->I, 8

The original used Latin letters for predicates; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including  ph and uses the Metamath equivalents of the natural deduction rules. (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.)

 |-  ( ph  ->  ( ps  ->  ch ) )   &    |-  ( ph  ->  ( ch  ->  th ) )   =>    |-  ( ph  ->  ( ps  ->  ( ch  /\  th ) ) )
 
9-Feb-2017ex-natded5.2i 20651 The same as ex-natded5.2 20649 and ex-natded5.2-2 20650 but with no context. (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ( ps  /\  ch )  ->  th )   &    |-  ( ch  ->  ps )   &    |-  ch   =>    |- 
 th
 
9-Feb-2017ex-natded5.2-2 20650 A more efficient proof of Theorem 5.2 of [Laboreo] p. 15. Compare with ex-natded5.2 20649 and ex-natded5.2i 20651. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ph  ->  (
 ( ps  /\  ch )  ->  th ) )   &    |-  ( ph  ->  ( ch  ->  ps ) )   &    |-  ( ph  ->  ch )   =>    |-  ( ph  ->  th )
 
9-Feb-2017ex-natded5.2 20649 Theorem 5.2 of [Laboreo] p. 15, translated line by line using the interpretation of natural deduction in Metamath. For information about ND and Metamath, see the page on Deduction Form and Natural Deduction in Metamath Proof Explorer. The original proof, which uses Fitch style, was written as follows:
#MPE#ND Expression MPE TranslationND Rationale MPE Rationale
15  ( ( ps  /\  ch )  ->  th )  ( ph  ->  ( ( ps  /\  ch )  ->  th ) ) Given $e.
22  ( ch  ->  ps )  ( ph  ->  ( ch  ->  ps ) ) Given $e.
31  ch  ( ph  ->  ch ) Given $e.
43  ps  ( ph  ->  ps )  ->E 2,3 mpd 16, the MPE equivalent of  ->E, 1,2
54  ( ps  /\  ch )  ( ph  ->  ( ps  /\  ch ) )  /\I 4,3 jca 520, the MPE equivalent of  /\I, 3,1
66  th  ( ph  ->  th )  ->E 1,5 mpd 16, the MPE equivalent of  ->E, 4,5

The original used Latin letters for predicates; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including  ph and uses the Metamath equivalents of the natural deduction rules. Below is the final metamath proof (which reorders some steps). A much more efficient proof, using more of Metamath and MPE's capabilities, is shown in ex-natded5.2-2 20650. A proof without context is shown in ex-natded5.2i 20651. (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.)

 |-  ( ph  ->  (
 ( ps  /\  ch )  ->  th ) )   &    |-  ( ph  ->  ( ch  ->  ps ) )   &    |-  ( ph  ->  ch )   =>    |-  ( ph  ->  th )
 
9-Feb-2017a4esbcd 3003 form of a4sbc 2933. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ph  ->  [. A  /  x ]. ps )   =>    |-  ( ph  ->  E. x ps )
 
9-Feb-2017a4sbcd 2934 Specialization: if a formula is true for all sets, it is true for any class which is a set. Similar to Theorem 6.11 of [Quine] p. 44. See also stdpc4 1896 and ra4sbc 2999. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ph  ->  A  e.  V )   &    |-  ( ph  ->  A. x ps )   =>    |-  ( ph  ->  [. A  /  x ]. ps )
 
9-Feb-2017sbceq1dd 2927 Equality theorem for class substitution. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  [. A  /  x ]. ph )   =>    |-  ( ph  ->  [. B  /  x ]. ph )
 
9-Feb-2017sbceq1d 2926 Equality theorem for class substitution. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ph  ->  A  =  B )   =>    |-  ( ph  ->  ( [. A  /  x ].
 ph 
 <-> 
 [. B  /  x ].
 ph ) )
 
9-Feb-2017exlimdd 1933 Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |- 
 F/ x ph   &    |-  F/ x ch   &    |-  ( ph  ->  E. x ps )   &    |-  (
 ( ph  /\  ps )  ->  ch )   =>    |-  ( ph  ->  ch )
 
9-Feb-2017pm2.21fal 1331 If a wff and its negation are provable, then falsum is provable. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ph  ->  ps )   &    |-  ( ph  ->  -.  ps )   =>    |-  ( ph  ->  F.  )
 
9-Feb-2017efald 1330 Deduction based on reductio ad absurdum. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ( ph  /\  -.  ps )  ->  F.  )   =>    |-  ( ph  ->  ps )
 
9-Feb-2017inegd 1329 Negation introduction rule from natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ( ph  /\  ps )  ->  F.  )   =>    |-  ( ph  ->  -. 
 ps )
 
9-Feb-2017dfnot 1328 Given falsum, we can define the negation of a wff  ph as the statement that a contradiction follows from assuming  ph. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( -.  ph  <->  ( ph  ->  F.  ) )
 
9-Feb-2017falimd 1326  F. implies anything. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ( ph  /\  F.  )  ->  ps )
 
9-Feb-2017pm2.18da 432 Deduction based on reductio ad absurdum. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ( ph  /\  -.  ps )  ->  ps )   =>    |-  ( ph  ->  ps )
 
9-Feb-2017pm2.01da 431 Deduction based on reductio ad absurdum. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ( ph  /\  ps )  ->  -.  ps )   =>    |-  ( ph  ->  -.  ps )
 
9-Feb-2017exmidd 407 Law of excluded middle in a context. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ph  ->  ( ps  \/  -.  ps )
 )
 
9-Feb-2017pm2.21dd 101 A contradiction implies anything. Deduction from pm2.21 102. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ph  ->  ps )   &    |-  ( ph  ->  -.  ps )   =>    |-  ( ph  ->  ch )
 
8-Feb-2017notnotrd 107 Deduction converting double-negation into the original wff, aka the double negation rule. A translation of natural deduction rule  -.  -. -C,  _G |-  -.  -.  ps =>  _G |-  ps; see natded 4. THis is definition NNC in [Pfenning] p. 17. This rule is valid in classical logic (which MPE uses), but not intuitionistic logic. (Contributed by DAW, 8-Feb-2017.)
 |-  ( ph  ->  -.  -.  ps )   =>    |-  ( ph  ->  ps )
 
5-Feb-2017eelT 27238 An elimination deduction. (Contributed by Alan Sare, 5-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (  T.  ->  ph )   &    |-  ( ph  ->  ps )   =>    |- 
 ps
 
4-Feb-20173impdirp1 27281 A deduction unionizing a non-unionized collection of virtual hypotheses. 3impdir 1243 is ~? uun3132 and is in set.mm. 3impdirp1 27281 is ~? uun3132p1. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ( ch  /\  ps )  /\  ( ph  /\ 
 ps ) )  ->  th )   =>    |-  ( ( ph  /\  ch  /\ 
 ps )  ->  th )
 
4-Feb-2017uun2221p2 27280 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ( ps  /\  ph )  /\  ph  /\  ph )  ->  ch )   =>    |-  ( ( ps  /\  ph )  ->  ch )
 
4-Feb-2017uun2221p1 27279 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  ( ps 
 /\  ph )  /\  ph )  ->  ch )   =>    |-  ( ( ps  /\  ph )  ->  ch )
 
4-Feb-2017uun123p4 27277 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ch  /\  ps  /\  ph )  ->  th )   =>    |-  (
 ( ph  /\  ps  /\  ch )  ->  th )
 
4-Feb-2017uun123p3 27276 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ps  /\  ch  /\  ph )  ->  th )   =>    |-  (
 ( ph  /\  ps  /\  ch )  ->  th )
 
4-Feb-2017uun123p2 27275 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ch  /\  ph  /\  ps )  ->  th )   =>    |-  ( ( ph  /\  ps  /\ 
 ch )  ->  th )
 
4-Feb-2017uun123p1 27274 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ps  /\  ph  /\  ch )  ->  th )   =>    |-  ( ( ph  /\  ps  /\ 
 ch )  ->  th )
 
4-Feb-2017uun123 27273 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  ch  /\  ps )  ->  th )   =>    |-  (
 ( ph  /\  ps  /\  ch )  ->  th )
 
4-Feb-20173anidm12p2 27272 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ps  /\  ph  /\  ph )  ->  ch )   =>    |-  ( ( ph  /\  ps )  ->  ch )
 
4-Feb-20173anidm12p1 27271 A deduction unionizing a non-unionized collection of virtual hypotheses. 3anidm12 1244 denotes the deduction which would have been named uun112 if it did not pre-exist in set.mm. This second permutation's name is based on this pre-existing name. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  ps  /\  ph )  ->  ch )   =>    |-  (
 ( ph  /\  ps )  ->  ch )
 
4-Feb-2017uun111 27270 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  ph  /\  ph )  ->  ps )   =>    |-  ( ph  ->  ps )
 
4-Feb-2017uunT12p5 27269 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ps  /\  ph  /\  T.  )  ->  ch )   =>    |-  ( ( ph  /\  ps )  ->  ch )
 
4-Feb-2017uunT12p4 27268 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  ps  /\  T.  )  ->  ch )   =>    |-  (
 ( ph  /\  ps )  ->  ch )
 
4-Feb-2017uunT12p3 27267 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ps  /\  T.  /\  ph )  ->  ch )   =>    |-  (
 ( ph  /\  ps )  ->  ch )
 
4-Feb-2017uunT12p2 27266 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  T.  /\  ps )  ->  ch )   =>    |-  (
 ( ph  /\  ps )  ->  ch )
 
4-Feb-2017uunT12p1 27265 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 (  T.  /\  ps  /\  ph )  ->  ch )   =>    |-  (
 ( ph  /\  ps )  ->  ch )
 
4-Feb-2017uunT12 27264 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 (  T.  /\  ph  /\  ps )  ->  ch )   =>    |-  ( ( ph  /\  ps )  ->  ch )
 
4-Feb-2017uunT11p2 27263 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  ph  /\  T.  )  ->  ps )   =>    |-  ( ph  ->  ps )
 
4-Feb-2017uunT11p1 27262 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  T.  /\  ph )  ->  ps )   =>    |-  ( ph  ->  ps )
 
4-Feb-2017uunT11 27261 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 (  T.  /\  ph  /\  ph )  ->  ps )   =>    |-  ( ph  ->  ps )
 
4-Feb-2017uunTT1p2 27260 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  T.  /\  T.  )  ->  ps )   =>    |-  ( ph  ->  ps )
 
4-Feb-2017uunTT1p1 27259 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 (  T.  /\  ph  /\  T.  )  ->  ps )   =>    |-  ( ph  ->  ps )
 
4-Feb-2017uunTT1 27258 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 (  T.  /\  T.  /\  ph )  ->  ps )   =>    |-  ( ph  ->  ps )
 
4-Feb-2017uun2131p1 27257 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ( ph  /\  ch )  /\  ( ph  /\  ps ) )  ->  th )   =>    |-  (
 ( ph  /\  ps  /\  ch )  ->  th )
 
4-Feb-2017uun2131 27256 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ( ph  /\  ps )  /\  ( ph  /\  ch ) )  ->  th )   =>    |-  (
 ( ph  /\  ps  /\  ch )  ->  th )
 
4-Feb-2017anabss7p1 27252 A deduction unionizing a non-unionized collection of virtual hypotheses. This would have been named uun221 if the 0th permutation did not exist in set.mm as anabss7 797. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ( ps  /\  ph )  /\  ph )  ->  ch )   =>    |-  ( ( ps  /\  ph )  ->  ch )
 
4-Feb-2017uun132p1 27251 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ( ps  /\  ch )  /\  ph )  ->  th )   =>    |-  ( ( ph  /\  ps  /\ 
 ch )  ->  th )
 
4-Feb-2017uun132 27250 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  ( ps 
 /\  ch ) )  ->  th )   =>    |-  ( ( ph  /\  ps  /\ 
 ch )  ->  th )
 
4-Feb-2017uun121p1 27249 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ( ph  /\  ps )  /\  ph )  ->  ch )   =>    |-  (
 ( ph  /\  ps )  ->  ch )
 
4-Feb-2017uun121 27248 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  ( ph  /\ 
 ps ) )  ->  ch )   =>    |-  ( ( ph  /\  ps )  ->  ch )
 
4-Feb-2017uunT1p1 27246 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  T.  )  ->  ps )   =>    |-  ( ph  ->  ps )
 
4-Feb-2017eelT0 27240 An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (  T.  ->  ph )   &    |-  ps   &    |-  ( ( ph  /\ 
 ps )  ->  ch )   =>    |-  ch
 
4-Feb-2017eel0cT 27239 An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ph   &    |-  ( ph  ->  ps )   =>    |-  (  T.  ->  ps )
 
4-Feb-2017eelTT 27236 An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (  T.  ->  ph )   &    |-  (  T.  ->  ps )   &    |-  ( ( ph  /\ 
 ps )  ->  ch )   =>    |-  ch
 
4-Feb-2017eel00cT 27235 An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ph   &    |-  ps   &    |-  ( ( ph  /\ 
 ps )  ->  ch )   =>    |-  (  T.  ->  ch )
 
4-Feb-2017eel0T1 27180 An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ph   &    |-  (  T.  ->  ps )   &    |-  ( ch  ->  th )   &    |-  ( ( ph  /\ 
 ps  /\  th )  ->  ta )   =>    |-  ( ch  ->  ta )
 
4-Feb-2017eelT01 27179 An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (  T.  ->  ph )   &    |-  ps   &    |-  ( ch  ->  th )   &    |-  ( ( ph  /\ 
 ps  /\  th )  ->  ta )   =>    |-  ( ch  ->  ta )
 
4-Feb-2017eelTT1 27178 An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (  T.  ->  ph )   &    |-  (  T.  ->  ps )   &    |-  ( ch  ->  th )   &    |-  ( ( ph  /\ 
 ps  /\  th )  ->  ta )   =>    |-  ( ch  ->  ta )
 
4-Feb-2017eelT12 27176 An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (  T.  ->  ph )   &    |-  ( ps  ->  ch )   &    |-  ( th  ->  ta )   &    |-  ( ( ph  /\ 
 ch  /\  ta )  ->  et )   =>    |-  ( ( ps  /\  th )  ->  et )
 
4-Feb-2017eelT11 27173 A elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (  T.  ->  ph )   &    |-  ( ps  ->  ch )   &    |-  ( ps  ->  th )   &    |-  ( ( ph  /\ 
 ch  /\  th )  ->  ta )   =>    |-  ( ps  ->  ta )
 
4-Feb-2017eelTTT 27171 An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (  T.  ->  ph )   &    |-  (  T.  ->  ps )   &    |-  (  T.  ->  ch )   &    |-  ( ( ph  /\ 
 ps  /\  ch )  ->  th )   =>    |- 
 th
 
4-Feb-2017eelT00 27170 An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (  T.  ->  ph )   &    |-  ps   &    |-  ch   &    |-  ( ( ph  /\ 
 ps  /\  ch )  ->  th )   =>    |- 
 th
 
4-Feb-2017eel0TT 27169 An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ph   &    |-  (  T.  ->  ps )   &    |-  (  T.  ->  ch )   &    |-  ( ( ph  /\ 
 ps  /\  ch )  ->  th )   =>    |- 
 th
 
4-Feb-2017eel000cT 27168 An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ph   &    |-  ps   &    |-  ch   &    |-  ( ( ph  /\ 
 ps  /\  ch )  ->  th )   =>    |-  (  T.  ->  th )
 
4-Feb-2017sbtT 27029 A substitution into a theorem remains true. sbt 1905 with the existence of no virtual hypotheses for the hypothesis expressed as the empty virtual hypothesis collection. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (  T.  ->  ph )   =>    |- 
 [ y  /  x ] ph
 
4-Feb-2017natded 4 Here are typical natural deduction (ND) rules in the style of Gentzen and Jaśkowski, along with MPE translations of them. This also shows the recommended theorems when you find yourself needing these rules (the recommendations encourage a slightly different proof style that works more naturally with metamath). A decent list of the standard rules of natural deduction can be found beginning with definition /\I in [Pfenning] p. 18. For information about ND and Metamath, see the page on Deduction Form and Natural Deduction in Metamath Proof Explorer. Many more citations could be added.

NameNatural Deduction RuleTranslation RecommendationComments
IT  _G |-  ps =>  _G |-  ps idi 2 nothing Reiteration is always redundant in Metamath. Definition "new rule" in [Pfenning] p. 18, definition IT in [Laboreo] p. 10.
 /\I  _G |-  ps &  _G |-  ch =>  _G |-  ps  /\  ch jca 520 jca 520, pm3.2i 443 Definition  /\I in [Pfenning] p. 18, definition I /\m,n in [Laboreo] p. 10, and definition  /\I in [Indrzejczak] p. 34 (representing both Gentzen's system NK and Jaśkowski)
 /\EL  _G |-  ps  /\  ch =>  _G |-  ps simpld 447 simpld 447, adantr 453 Definition  /\EL in [Pfenning] p. 18, definition E /\(1) in [Laboreo] p. 11, and definition  /\E in [Indrzejczak] p. 34 (representing both Gentzen's system NK and Jaśkowski)
 /\ER  _G |-  ps  /\  ch =>  _G |-  ch simprd 451 simpr 449, adantl 454 Definition  /\ER in [Pfenning] p. 18, definition E /\(2) in [Laboreo] p. 11, and definition  /\E in [Indrzejczak] p. 34 (representing both Gentzen's system NK and Jaśkowski)
 ->I  _G ,  ps |-  ch =>  _G |-  ps  ->  ch ex 425 ex 425 Definition  ->I in [Pfenning] p. 18, definition I=>m,n in [Laboreo] p. 11, and definition  ->I in [Indrzejczak] p. 33.
 ->E  _G |-  ps  ->  ch &  _G |-  ps =>  _G |-  ch mpd 16 ax-mp 10, mpd 16, mpdan 652, imp 420 Definition  ->E in [Pfenning] p. 18, definition E=>m,n in [Laboreo] p. 11, and definition  ->E in [Indrzejczak] p. 33.
 \/IL  _G |-  ps =>  _G |-  ps  \/  ch olcd 384 olc 375, olci 382, olcd 384 Definition  \/I in [Pfenning] p. 18, definition I \/n(1) in [Laboreo] p. 12
 \/IR  _G |-  ch =>  _G |-  ps  \/  ch orcd 383 orc 376, orci 381, orcd 383 Definition  \/IR in [Pfenning] p. 18, definition I \/n(2) in [Laboreo] p. 12.
 \/E  _G |-  ps  \/  ch &  _G ,  ps |-  th &  _G ,  ch |-  th =>  _G |-  th mpjaodan 764 mpjaodan 764, jaodan 763, jaod 371 Definition  \/E in [Pfenning] p. 18, definition E \/m,n,p in [Laboreo] p. 12.
 -.I  _G ,  ps |-  F. =>  _G |-  -.  ps inegd 1329 pm2.01d 163
 -.I  _G ,  ps |-  th &  _G |-  -.  th =>  _G |-  -.  ps mtand 643 mtand 643 definition I -.m,n,p in [Laboreo] p. 13.
 -.I  _G ,  ps |-  ch &  _G ,  ps |-  -.  ch =>  _G |-  -.  ps pm2.65da 562 pm2.65da 562 Contradiction.
 -.I  _G ,  ps |-  -.  ps =>  _G |-  -.  ps pm2.01da 431 pm2.01d 163, pm2.65da 562, pm2.65d 168 For an alternative falsum-free natural deduction ruleset
 -.E  _G |-  ps &  _G |-  -.  ps =>  _G |-  F. pm2.21fal 1331 pm2.21dd 101
 -.E  _G ,  -.  ps |-  F. =>  _G |-  ps pm2.21dd 101 definition  ->E in [Indrzejczak] p. 33.
 -.E  _G |-  ps &  _G |-  -.  ps =>  _G |-  th pm2.21dd 101 pm2.21dd 101, pm2.21d 100, pm2.21 102 For an alternative falsum-free natural deduction ruleset. Definition  -.E in [Pfenning] p. 18.
 T.I  _G |-  T. a1tru 1327 tru 1317, a1tru 1327, trud 1320 Definition  T.I in [Pfenning] p. 18.
 F.E  _G ,  F.  |-  th falimd 1326 falim 1325 Definition  F.E in [Pfenning] p. 18.
 A.I  _G |-  [ a  /  x ] ps =>  _G |-  A. x ps alrimiv 2012 alrimiv 2012, ralrimiva 2588 Definition  A.Ia in [Pfenning] p. 18, definition I A.n in [Laboreo] p. 32.
 A.E  _G |-  A. x ps =>  _G |-  [ t  /  x ] ps a4sbcd 2934 cla4v 2811, rcla4v 2817 Definition  A.E in [Pfenning] p. 18, definition E A.n,t in [Laboreo] p. 32.
 E.I  _G |-  [ t  /  x ] ps =>  _G |-  E. x ps a4esbcd 3003 cla4ev 2812, rcla4ev 2821 Definition  E.I in [Pfenning] p. 18, definition I E.n,t in [Laboreo] p. 32.
 E.E  _G |-  E. x ps &  _G ,  [ a  /  x ] ps |-  th =>  _G |-  th exlimddv 1934 exlimddv 1934, exlimdd 1933, exlimdv 1932, rexlimdva 2629 Definition  E.Ea,u in [Pfenning] p. 18, definition E E.m,n,p,a in [Laboreo] p. 32.
 F.C  _G ,  -.  ps |-  F. =>  _G |-  ps efald 1330 efald 1330 Proof by contradiction (classical logic), definition  F.C in [Pfenning] p. 17.
 F.C  _G ,  -.  ps |-  ps =>  _G |-  ps pm2.18da 432 pm2.18da 432, pm2.18d 105, pm2.18 104 For an alternative falsum-free natural deduction ruleset
 -.  -.C  _G |-  -.  -.  ps =>  _G |-  ps notnotrd 107 notnotrd 107, notnot2 106 Double negation rule (classical logic), definition NNC in [Pfenning] p. 17, definition E -.n in [Laboreo] p. 14.
EM  _G |-  ps  \/  -.  ps exmidd 407 exmid 406 Excluded middle (classical logic), definition XM in [Pfenning] p. 17, proof 5.11 in [Laboreo] p. 14.
 =I  _G |-  A  =  A eqidd 2254 eqid 2253, eqidd 2254 Introduce equality, definition =I in [Pfenning] p. 127.
 =E  _G |-  A  =  B &  _G [. A  /  x ]. ps =>  _G |-  [. B  /  x ]. ps sbceq1dd 2927 sbceq1d 2926, equality theorems Eliminate equality, definition =E in [Pfenning] p. 127. (Both E1 and E2.)

Note that MPE uses classical logic, not intuitionist logic. As is conventional, the "I" rules are introduction rules, "E" rules are elimination rules, the "C" rules are conversion rules, and  _G represents the set of (current) hypotheses. We use wff variable names beginning with  ps to provide a closer representation of the Metamath equivalents (which typically use the antedent  ph to represent the context  _G).

Most of this information was developed by Mario Carneiro and posted on 3-Feb-2017. For more information, see the page on Deduction Form and Natural Deduction in Metamath Proof Explorer.

For annotated examples where some traditional ND rules are directly applied in MPE, see ex-natded5.2 20649, ex-natded5.3 20652, ex-natded5.5 20655, ex-natded5.7 20656, ex-natded5.8 20658, ex-natded5.13 20660, ex-natded9.20 20662, and ex-natded9.26 20664.

(Contributed by DAW, 4-Feb-2017.)

 |-  ph   =>    |-  ph
 
31-Jan-20172p2ne5 26953 Prove that  2  +  2  =/=  5. In George Orwell's "1984", Part One, Chapter Seven, the protagonist Winston notes that, "In the end the Party would announce that two and two made five, and you would have to believe it." http://www.sparknotes.com/lit/1984/section4.rhtml. More generally, the phrase  2  +  2  =  5 has come to represent an obviously false dogma one may be required to believe. See the Wikipedia article for more about this: https://en.wikipedia.org/wiki/2_%2B_2_%3D_5. Unsurprisingly, we can easily prove that this claim is false. (Contributed by David A. Wheeler, 31-Jan-2017.)
 |-  (
 2  +  2 )  =/=  5
 
31-Jan-20175m4e1 26952 Prove that 5 - 4 = 1. (Contributed by David A. Wheeler, 31-Jan-2017.)
 |-  (
 5  -  4 )  =  1
 
30-Jan-2017yoniso 13903 If the codomain is recoverable from a hom-set, then the Yoneda embedding is injective on objects, and hence is an isomorphism from  C into a full subcategory of a presheaf category. (Contributed by Mario Carneiro, 30-Jan-2017.)
 |-  Y  =  (Yon `  C )   &    |-  O  =  (oppCat `  C )   &    |-  S  =  (
 SetCat `  U )   &    |-  D  =  (CatCat `  V )   &    |-  B  =  ( Base `  D )   &    |-  I  =  (  Iso  `  D )   &    |-  Q  =  ( O FuncCat  S )   &    |-  E  =  ( Qs 
 ran  ( 1st `  Y ) )   &    |-  ( ph  ->  V  e.  X )   &    |-  ( ph  ->  C  e.  B )   &    |-  ( ph  ->  U  e.  W )   &    |-  ( ph  ->  ran  (  Homf  `  C )  C_  U )   &    |-  ( ph  ->  E  e.  B )   &    |-  ( ( ph  /\  ( x  e.  ( Base `  C )  /\  y  e.  ( Base `  C ) ) ) 
 ->  ( F `  ( x (  Hom  `  C ) y ) )  =  y )   =>    |-  ( ph  ->  Y  e.  ( C I E ) )
 
30-Jan-2017fullres2c 13657 Condition for a full functor to also be a full functor into the restriction. (Contributed by Mario Carneiro, 30-Jan-2017.)
 |-  A  =  ( Base `  C )   &    |-  E  =  ( Ds  S )   &    |-  ( ph  ->  D  e.  Cat )   &    |-  ( ph  ->  S  e.  V )   &    |-  ( ph  ->  F : A --> S )   =>    |-  ( ph  ->  ( F ( C Full  D ) G  <->  F ( C Full  E ) G ) )
 
30-Jan-2017fthres2c 13649 Condition for a faithful functor to also be a faithful functor into the restriction. (Contributed by Mario Carneiro, 30-Jan-2017.)
 |-  A  =  ( Base `  C )   &    |-  E  =  ( Ds  S )   &    |-  ( ph  ->  D  e.  Cat )   &    |-  ( ph  ->  S  e.  V )   &    |-  ( ph  ->  F : A --> S )   =>    |-  ( ph  ->  ( F ( C Faith  D ) G  <->  F ( C Faith  E ) G ) )
 
30-Jan-2017funcres2c 13619 Condition for a functor to also be a functor into the restriction. (Contributed by Mario Carneiro, 30-Jan-2017.)
 |-  A  =  ( Base `  C )   &    |-  E  =  ( Ds  S )   &    |-  ( ph  ->  D  e.  Cat )   &    |-  ( ph  ->  S  e.  V )   &    |-  ( ph  ->  F : A --> S )   =>    |-  ( ph  ->  ( F ( C  Func  D ) G  <->  F ( C  Func  E ) G ) )
 
29-Jan-2017yonffth 13902 The Yoneda Lemma. The Yoneda embedding, the curried Hom functor, is full and faithful, and hence is a representation of the category  C as a full subcategory of the category  Q of presheaves on  C. (Contributed by Mario Carneiro, 29-Jan-2017.)
 |-  Y  =  (Yon `  C )   &    |-  O  =  (oppCat `  C )   &    |-  S  =  (
 SetCat `  U )   &    |-  Q  =  ( O FuncCat  S )   &    |-  ( ph  ->  C  e.  Cat )   &    |-  ( ph  ->  U  e.  V )   &    |-  ( ph  ->  ran  (  Homf  `  C )  C_  U )   =>    |-  ( ph  ->  Y  e.  ( ( C Full  Q )  i^i  ( C Faith  Q ) ) )
 
29-Jan-2017yoneda 13901 The Yoneda Lemma. There is a natural isomorphism between the functors  Z and  E, where  Z ( F ,  X ) is the natural transformations from Yon ( X )  =  Hom  (  -  ,  X ) to  F, and  E ( F ,  X )  =  F ( X ) is the evaluation functor. Here we need two universes to state the claim: the smaller universe  U is used for forming the functor category  Q  =  C op  ->  SetCat ( U ), which itself does not (necessarily) live in  U but instead is an element of the larger universe  V. (If  U is a Grothendieck universe, then it will be closed under this "presheaf" operation, and so we can set  U  =  V in this case.) (Contributed by Mario Carneiro, 29-Jan-2017.)
 |-  Y  =  (Yon `  C )   &    |-  B  =  (
 Base `  C )   &    |-  .1.  =  ( Id `  C )   &    |-  O  =  (oppCat `  C )   &    |-  S  =  ( SetCat `  U )   &    |-  T  =  (
 SetCat `  V )   &    |-  Q  =  ( O FuncCat  S )   &    |-  H  =  (HomF `  Q )   &    |-  R  =  ( ( Q  X.c  O ) FuncCat  T )   &    |-  E  =  ( O evalF 
 S )   &    |-  Z  =  ( H  o.func  ( ( <. ( 1st `  Y ) , tpos  ( 2nd `  Y ) >.  o.func  ( Q  2ndF  O ) ) ⟨,⟩F  ( Q  1stF  O )
 ) )   &    |-  ( ph  ->  C  e.  Cat )   &    |-  ( ph  ->  V  e.  W )   &    |-  ( ph  ->  ran  (  Homf  `  C )  C_  U )   &    |-  ( ph  ->  ( ran  (  Homf  `  Q )  u.  U )  C_  V )   &    |-  M  =  ( f  e.  ( O  Func  S ) ,  x  e.  B  |->  ( a  e.  ( ( ( 1st `  Y ) `  x ) ( O Nat  S ) f )  |->  ( ( a `
  x ) `  (  .1.  `  x )
 ) ) )   &    |-  I  =  (  Iso  `  R )   =>    |-  ( ph  ->  M  e.  ( Z I E ) )
 
29-Jan-2017yonffthlem 13900 Lemma for yonffth 13902. (Contributed by Mario Carneiro, 29-Jan-2017.)
 |-  Y  =  (Yon `  C )   &    |-  B  =  (
 Base `  C )   &    |-  .1.  =  ( Id `  C )   &    |-  O  =  (oppCat `  C )   &    |-  S  =  ( SetCat `  U )   &    |-  T  =  (
 SetCat `  V )   &    |-  Q  =  ( O FuncCat  S )   &    |-  H  =  (HomF `  Q )   &    |-  R  =  ( ( Q  X.c  O ) FuncCat  T )   &    |-  E  =  ( O evalF 
 S )   &    |-  Z  =  ( H  o.func  ( ( <. ( 1st `  Y ) , tpos  ( 2nd `  Y ) >.  o.func  ( Q  2ndF  O ) ) ⟨,⟩F  ( Q  1stF  O )
 ) )   &    |-  ( ph  ->  C  e.  Cat )   &    |-  ( ph  ->  V  e.  W )   &    |-  ( ph  ->  ran  (  Homf  `  C )  C_  U )   &    |-  ( ph  ->  ( ran  (  Homf  `  Q )  u.  U )  C_  V )   &    |-  M  =  ( f  e.  ( O  Func  S ) ,  x  e.  B  |->  ( a  e.  ( ( ( 1st `  Y ) `  x ) ( O Nat  S ) f )  |->  ( ( a `
  x ) `  (  .1.  `  x )
 ) ) )   &    |-  I  =  (Inv `  R )   &    |-  N  =  ( f  e.  ( O  Func  S ) ,  x  e.  B  |->  ( u  e.  ( ( 1st `  f ) `  x )  |->  ( y  e.  B  |->  ( g  e.  ( y ( 
 Hom  `  C ) x )  |->  ( ( ( x ( 2nd `  f ) y ) `
  g ) `  u ) ) ) ) )   =>    |-  ( ph  ->  Y  e.  ( ( C Full  Q )  i^i  ( C Faith  Q ) ) )
 
29-Jan-2017yonedainv 13899 The Yoneda Lemma with explicit inverse. (Contributed by Mario Carneiro, 29-Jan-2017.)
 |-  Y  =  (Yon `  C )   &    |-  B  =  (
 Base `  C )   &    |-  .1.  =  ( Id `  C )   &    |-  O  =  (oppCat `  C )   &    |-  S  =  ( SetCat `  U )   &    |-  T  =  (
 SetCat `  V )   &    |-  Q  =  ( O FuncCat  S )   &    |-  H  =  (HomF `  Q )   &    |-  R  =  ( ( Q  X.c  O ) FuncCat  T )   &    |-  E  =  ( O evalF 
 S )   &    |-  Z  =  ( H  o.func  ( ( <. ( 1st `  Y ) , tpos  ( 2nd `  Y ) >.  o.func  ( Q  2ndF  O ) ) ⟨,⟩F  ( Q  1stF  O )
 ) )   &    |-  ( ph  ->  C  e.  Cat )   &    |-  ( ph  ->  V  e.  W )   &    |-  ( ph  ->  ran  (  Homf  `  C )  C_  U )   &    |-  ( ph  ->  ( ran  (  Homf  `  Q )  u.  U )  C_  V )   &    |-  M  =  ( f  e.  ( O  Func  S ) ,  x  e.  B  |->  ( a  e.  ( ( ( 1st `  Y ) `  x ) ( O Nat  S ) f )  |->  ( ( a `
  x ) `  (  .1.  `  x )
 ) ) )   &    |-  I  =  (Inv `  R )   &    |-  N  =  ( f  e.  ( O  Func  S ) ,  x  e.  B  |->  ( u  e.  ( ( 1st `  f ) `  x )  |->  ( y  e.  B  |->  ( g  e.  ( y ( 
 Hom  `  C ) x )  |->  ( ( ( x ( 2nd `  f ) y ) `
  g ) `  u ) ) ) ) )   =>    |-  ( ph  ->  M ( Z I E ) N )
 
29-Jan-2017yonedalem3b 13897 Lemma for yoneda 13901. (Contributed by Mario Carneiro, 29-Jan-2017.)
 |-  Y  =  (Yon `  C )   &    |-  B  =  (
 Base `  C )   &    |-  .1.  =  ( Id `  C )   &    |-  O  =  (oppCat `  C )   &    |-  S  =  ( SetCat `  U )   &    |-  T  =  (
 SetCat `  V )   &    |-  Q  =  ( O FuncCat  S )   &    |-  H  =  (HomF `  Q )   &    |-  R  =  ( ( Q  X.c  O ) FuncCat  T )   &    |-  E  =  ( O evalF 
 S )   &    |-  Z  =  ( H  o.func  ( ( <. ( 1st `  Y ) , tpos  ( 2nd `  Y ) >.  o.func  ( Q  2ndF  O ) ) ⟨,⟩F  ( Q  1stF  O )
 ) )   &    |-  ( ph  ->  C  e.  Cat )   &    |-  ( ph  ->  V  e.  W )   &    |-  ( ph  ->  ran  (  Homf  `  C )  C_  U )   &    |-  ( ph  ->  ( ran  (  Homf  `  Q )  u.  U )  C_  V )   &    |-  ( ph  ->  F  e.  ( O  Func  S ) )   &    |-  ( ph  ->  X  e.  B )   &    |-  ( ph  ->  G  e.  ( O  Func  S ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  A  e.  ( F ( O Nat  S ) G ) )   &    |-  ( ph  ->  K  e.  ( P (  Hom  `  C ) X ) )   &    |-  M  =  ( f  e.  ( O  Func  S ) ,  x  e.  B  |->  ( a  e.  ( ( ( 1st `  Y ) `  x ) ( O Nat  S ) f )  |->  ( ( a `
  x ) `  (  .1.  `  x )
 ) ) )   =>    |-  ( ph  ->  ( ( G M P ) ( <. ( F ( 1st `  Z ) X ) ,  ( G ( 1st `  Z ) P ) >. (comp `  T ) ( G ( 1st `  E ) P ) ) ( A ( <. F ,  X >. ( 2nd `  Z ) <. G ,  P >. ) K ) )  =  ( ( A ( <. F ,  X >. ( 2nd `  E ) <. G ,  P >. ) K ) (
 <. ( F ( 1st `  Z ) X ) ,  ( F ( 1st `  E ) X ) >. (comp `  T ) ( G ( 1st `  E ) P ) ) ( F M X ) ) )
 
29-Jan-2017yonedalem22 13896 Lemma for yoneda 13901. (Contributed by Mario Carneiro, 29-Jan-2017.)
 |-  Y  =  (Yon `  C )   &    |-  B  =  (
 Base `  C )   &    |-  .1.  =  ( Id `  C )   &    |-  O  =  (oppCat `  C )   &    |-  S  =  ( SetCat `  U )   &    |-  T  =  (
 SetCat `  V )   &    |-  Q  =  ( O FuncCat  S )   &    |-  H  =  (HomF `  Q )   &    |-  R  =  ( ( Q  X.c  O ) FuncCat  T )   &    |-  E  =  ( O evalF 
 S )   &    |-  Z  =  ( H  o.func  ( ( <. ( 1st `  Y ) , tpos  ( 2nd `  Y ) >.  o.func  ( Q  2ndF  O ) ) ⟨,⟩F  ( Q  1stF  O )
 ) )   &    |-  ( ph  ->  C  e.  Cat )   &    |-  ( ph  ->  V  e.  W )   &    |-  ( ph  ->  ran  (  Homf  `  C )  C_  U )   &    |-  ( ph  ->  ( ran  (  Homf  `  Q )  u.  U )  C_  V )   &    |-  ( ph  ->  F  e.  ( O  Func  S ) )   &    |-  ( ph  ->  X  e.  B )   &    |-  ( ph  ->  G  e.  ( O  Func  S ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  A  e.  ( F ( O Nat  S ) G ) )   &    |-  ( ph  ->  K  e.  ( P (  Hom  `  C ) X ) )   =>    |-  ( ph  ->  ( A ( <. F ,  X >. ( 2nd `  Z ) <. G ,  P >. ) K )  =  ( ( ( P ( 2nd `  Y ) X ) `  K ) ( <. ( ( 1st `  Y ) `  X ) ,  F >. ( 2nd `  H ) <. ( ( 1st `  Y ) `  P ) ,  G >. ) A ) )
 
29-Jan-2017yonedalem4c 13895 Lemma for yoneda 13901. (Contributed by Mario Carneiro, 29-Jan-2017.)
 |-  Y  =  (Yon `  C )   &    |-  B  =  (
 Base `  C )   &    |-  .1.  =  ( Id `  C )   &    |-  O  =  (oppCat `  C )   &    |-  S  =  ( SetCat `  U )   &    |-  T  =  (
 SetCat `  V )   &    |-  Q  =  ( O FuncCat  S )   &    |-  H  =  (HomF `  Q )   &    |-  R  =  ( ( Q  X.c  O ) FuncCat  T )   &    |-  E  =  ( O evalF 
 S )   &    |-  Z  =  ( H  o.func  ( ( <. ( 1st `  Y ) , tpos  ( 2nd `  Y ) >.  o.func  ( Q  2ndF  O ) ) ⟨,⟩F  ( Q  1stF  O )
 ) )   &    |-  ( ph  ->  C  e.  Cat )   &    |-  ( ph  ->  V  e.  W )   &    |-  ( ph  ->  ran  (  Homf  `  C )  C_  U )   &    |-  ( ph  ->  ( ran  (  Homf  `  Q )  u.  U )  C_  V )   &    |-  ( ph  ->  F  e.  ( O  Func  S ) )   &    |-  ( ph  ->  X  e.  B )   &    |-  N  =  ( f  e.  ( O 
 Func  S ) ,  x  e.  B  |->  ( u  e.  ( ( 1st `  f
 ) `  x )  |->  ( y  e.  B  |->  ( g  e.  (
 y (  Hom  `  C ) x )  |->  ( ( ( x ( 2nd `  f ) y ) `
  g ) `  u ) ) ) ) )   &    |-  ( ph  ->  A  e.  ( ( 1st `  F ) `  X ) )   =>    |-  ( ph  ->  (
 ( F N X ) `  A )  e.  ( ( ( 1st `  Y ) `  X ) ( O Nat  S ) F ) )
 
29-Jan-2017yonedalem4b 13894 Lemma for yoneda 13901. (Contributed by Mario Carneiro, 29-Jan-2017.)
 |-  Y  =  (Yon `  C )   &    |-  B  =  (
 Base `  C )   &    |-  .1.  =  ( Id `  C )   &    |-  O  =  (oppCat `  C )   &    |-  S  =  ( SetCat `  U )   &    |-  T  =  (
 SetCat `  V )   &    |-  Q  =  ( O FuncCat  S )   &    |-  H  =  (HomF `  Q )   &    |-  R  =  ( ( Q  X.c  O ) FuncCat  T )   &    |-  E  =  ( O evalF 
 S )   &    |-  Z  =  ( H  o.func  ( ( <. ( 1st `  Y ) , tpos  ( 2nd `  Y ) >.  o.func  ( Q  2ndF  O ) ) ⟨,⟩F  ( Q  1stF  O )
 ) )   &    |-  ( ph  ->  C  e.  Cat )   &    |-  ( ph  ->  V  e.  W )   &    |-  ( ph  ->  ran  (  Homf  `  C )  C_  U )   &    |-  ( ph  ->  ( ran  (  Homf  `  Q )  u.  U )  C_  V )   &    |-  ( ph  ->  F  e.  ( O  Func  S ) )   &    |-  ( ph  ->  X  e.  B )   &    |-  N  =  ( f  e.  ( O 
 Func  S ) ,  x  e.  B  |->  ( u  e.  ( ( 1st `  f
 ) `  x )  |->  ( y  e.  B  |->  ( g  e.  (
 y (  Hom  `  C ) x )  |->  ( ( ( x ( 2nd `  f ) y ) `
  g ) `  u ) ) ) ) )   &    |-  ( ph  ->  A  e.  ( ( 1st `  F ) `  X ) )   &    |-  ( ph  ->  P  e.  B )   &    |-  ( ph  ->  G  e.  ( P (  Hom  `  C ) X ) )   =>    |-  ( ph  ->  ( ( ( ( F N X ) `  A ) `  P ) `  G )  =  ( ( ( X ( 2nd `  F ) P ) `  G ) `  A ) )
 
29-Jan-2017yonedalem4a 13893 Lemma for yoneda 13901. (Contributed by Mario Carneiro, 29-Jan-2017.)
 |-  Y  =  (Yon `  C )   &    |-  B  =  (
 Base `  C )   &    |-  .1.  =  ( Id `  C )   &    |-  O  =  (oppCat `  C )   &    |-  S  =  ( SetCat `  U )   &    |-  T  =  (
 SetCat `  V )   &    |-  Q  =  ( O FuncCat  S )   &    |-  H  =  (HomF `  Q )   &    |-  R  =  ( ( Q  X.c  O ) FuncCat  T )   &    |-  E  =  ( O evalF 
 S )   &    |-  Z  =  ( H  o.func  ( ( <. ( 1st `  Y ) , tpos  ( 2nd