Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  mp3an2i Unicode version

Theorem mp3an2i 1320
 Description: mp3an 1315 with antecedents in standard conjunction form and with two hypotheses which are implications. (Contributed by Alan Sare, 28-Aug-2016.)
Hypotheses
Ref Expression
mp3an2i.1
mp3an2i.2
mp3an2i.3
mp3an2i.4
Assertion
Ref Expression
mp3an2i

Proof of Theorem mp3an2i
StepHypRef Expression
1 mp3an2i.2 . 2
2 mp3an2i.3 . 2
3 mp3an2i.1 . . 3
4 mp3an2i.4 . . 3
53, 4mp3an1 1302 . 2
61, 2, 5syl2anc 408 1
 Colors of variables: wff set class Syntax hints:   wi 4   w3a 962 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116  df-3an 964 This theorem is referenced by:  mapen  6733  mapxpen  6735  en2eleq  7044  nnledivrp  9546  xsubge0  9657  frec2uzsucd  10167  seq3shft  10603  geolim2  11274  geoisum1c  11282  ntrivcvgap  11310  eflegeo  11397  sin01gt0  11457  cos01gt0  11458  gcdn0gt0  11655  divgcdodd  11810  sqpweven  11842  2sqpwodd  11843  ressid  12009  topnvalg  12121  restbasg  12326  restco  12332  lmfval  12350  cnfval  12352  cnpval  12356  upxp  12430  uptx  12432  txrest  12434  xblm  12575  bdmet  12660  bdmopn  12662  reopnap  12696  cnopnap  12752  dvidlemap  12818  dvcj  12831  trilpolemisumle  13220
 Copyright terms: Public domain W3C validator