Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ifan Structured version   Unicode version

Theorem ifan 3985
 Description: Rewrite a conjunction in an if statement as two nested conditionals. (Contributed by Mario Carneiro, 28-Jul-2014.)
Assertion
Ref Expression
ifan

Proof of Theorem ifan
StepHypRef Expression
1 iftrue 3945 . . 3
2 ibar 504 . . . 4
32ifbid 3961 . . 3
41, 3eqtr2d 2509 . 2
5 simpl 457 . . . . 5
65con3i 135 . . . 4
7 iffalse 3948 . . . 4
86, 7syl 16 . . 3
9 iffalse 3948 . . 3
108, 9eqtr4d 2511 . 2
114, 10pm2.61i 164 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wa 369   wceq 1379  cif 3939 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-if 3940 This theorem is referenced by:  itg0  22013  iblre  22027  itgreval  22030  iblss  22038  iblss2  22039  itgle  22043  itgss  22045  itgeqa  22047  iblconst  22051  itgconst  22052  ibladdlem  22053  iblabslem  22061  iblabsr  22063  iblmulc2  22064  itgsplit  22069  itgcn  22076  mrsubrn  28624  itg2gt0cn  29923  ibladdnclem  29924  iblabsnclem  29931  iblmulc2nc  29933  bddiblnc  29938  iblsplit  31511
 Copyright terms: Public domain W3C validator