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  1117  sbequilem  1760  unssi  3148  ssini  3196  bm1.3ii  3907  epelg  4053  onsucelsucexmid  4281  elvv  4428  funpr  4982  mpt2v  5625  caovcom  5689  th3q  6277  endisj  6368  phplem2  6388  addnnnq0  6701  mulnnnq0  6702  nqprxx  6798  addsrpr  6984  mulsrpr  6985  recidpirq  7088  apreim  7770  mulcanapi  7824  div1  7858  recdivap  7873  divdivap1  7878  divdivap2  7879  divassapi  7923  divdirapi  7924  div23api  7925  div11api  7926  divmuldivapi  7927  divmul13api  7928  divadddivapi  7929  divdivdivapi  7930  lemulge11  8011  negiso  8100  2cnne0  8307  2rene0  8308  1mhlfehlf  8316  halfpm6th  8318  2halves  8327  halfaddsub  8332  avglt1  8336  avglt2  8337  div4p1lem1div2  8351  3halfnz  8525  nneoor  8530  zeo  8533  divlt1lt  8882  divle1le  8883  nnledivrp  8918  2tnp1ge0ge0  9383  frecfzennn  9508  expge1  9610  faclbnd2  9766  4bc2eq6  9798  cjreb  9891  sqrt2gt1lt2  10073  amgm2  10142  3dvdsdec  10409  3dvds2dec  10410  odd2np1  10417  oddge22np1  10425  ltoddhalfle  10437  halfleoddlt  10438  nno  10450  ndvdsi  10477  flodddiv4  10478  flodddiv4lt  10480  flodddiv4t2lthalf  10481  3lcm2e6woprm  10612  6lcm4e12  10613  ex-an  10712  ex-fl  10714  bdbm1.3ii  10840
  Copyright terms: Public domain W3C validator