ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm3.2i GIF version

Theorem pm3.2i 266
Description: Infer conjunction of premises. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
pm3.2i.1 𝜑
pm3.2i.2 𝜓
Assertion
Ref Expression
pm3.2i (𝜑𝜓)

Proof of Theorem pm3.2i
StepHypRef Expression
1 pm3.2i.1 . 2 𝜑
2 pm3.2i.2 . 2 𝜓
3 pm3.2 137 . 2 (𝜑 → (𝜓 → (𝜑𝜓)))
41, 2, 3mp2 16 1 (𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106
This theorem is referenced by:  mp4an  418  pm4.87  524  biijust  603  3pm3.2i  1119  sbequilem  1763  unssi  3164  ssini  3212  bm1.3ii  3937  epelg  4093  onsucelsucexmid  4321  elvv  4470  funpr  5033  mpt2v  5697  caovcom  5761  th3q  6351  endisj  6494  phplem2  6523  addnnnq0  6955  mulnnnq0  6956  nqprxx  7052  addsrpr  7238  mulsrpr  7239  recidpirq  7342  apreim  8024  mulcanapi  8078  div1  8112  recdivap  8127  divdivap1  8132  divdivap2  8133  divassapi  8177  divdirapi  8178  div23api  8179  div11api  8180  divmuldivapi  8181  divmul13api  8182  divadddivapi  8183  divdivdivapi  8184  lemulge11  8265  negiso  8354  2cnne0  8561  2rene0  8562  1mhlfehlf  8570  halfpm6th  8572  2halves  8581  halfaddsub  8586  avglt1  8590  avglt2  8591  div4p1lem1div2  8605  3halfnz  8779  nneoor  8784  zeo  8787  divlt1lt  9136  divle1le  9137  nnledivrp  9172  2tnp1ge0ge0  9639  frecfzennn  9764  fxnn0nninf  9775  expge1  9894  faclbnd2  10050  4bc2eq6  10082  cjreb  10199  sqrt2gt1lt2  10381  amgm2  10450  3dvdsdec  10771  3dvds2dec  10772  odd2np1  10779  oddge22np1  10787  ltoddhalfle  10799  halfleoddlt  10800  nno  10812  ndvdsi  10839  flodddiv4  10840  flodddiv4lt  10842  flodddiv4t2lthalf  10843  3lcm2e6woprm  10974  6lcm4e12  10975  ex-an  11120  ex-fl  11122  bdbm1.3ii  11251
  Copyright terms: Public domain W3C validator