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

Theorem pm3.2i 266
Description: Infer conjunction of premises. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
pm3.2i.1  |-  ph
pm3.2i.2  |-  ps
Assertion
Ref Expression
pm3.2i  |-  ( ph  /\ 
ps )

Proof of Theorem pm3.2i
StepHypRef Expression
1 pm3.2i.1 . 2  |-  ph
2 pm3.2i.2 . 2  |-  ps
3 pm3.2 137 . 2  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
41, 2, 3mp2 16 1  |-  ( ph  /\ 
ps )
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  1761  unssi  3157  ssini  3205  bm1.3ii  3919  epelg  4073  onsucelsucexmid  4301  elvv  4448  funpr  5002  mpt2v  5645  caovcom  5709  th3q  6298  endisj  6389  phplem2  6409  addnnnq0  6753  mulnnnq0  6754  nqprxx  6850  addsrpr  7036  mulsrpr  7037  recidpirq  7140  apreim  7822  mulcanapi  7876  div1  7910  recdivap  7925  divdivap1  7930  divdivap2  7931  divassapi  7975  divdirapi  7976  div23api  7977  div11api  7978  divmuldivapi  7979  divmul13api  7980  divadddivapi  7981  divdivdivapi  7982  lemulge11  8063  negiso  8152  2cnne0  8359  2rene0  8360  1mhlfehlf  8368  halfpm6th  8370  2halves  8379  halfaddsub  8384  avglt1  8388  avglt2  8389  div4p1lem1div2  8403  3halfnz  8577  nneoor  8582  zeo  8585  divlt1lt  8934  divle1le  8935  nnledivrp  8970  2tnp1ge0ge0  9435  frecfzennn  9560  expge1  9662  faclbnd2  9818  4bc2eq6  9850  cjreb  9954  sqrt2gt1lt2  10136  amgm2  10205  3dvdsdec  10472  3dvds2dec  10473  odd2np1  10480  oddge22np1  10488  ltoddhalfle  10500  halfleoddlt  10501  nno  10513  ndvdsi  10540  flodddiv4  10541  flodddiv4lt  10543  flodddiv4t2lthalf  10544  3lcm2e6woprm  10675  6lcm4e12  10676  ex-an  10821  ex-fl  10823  bdbm1.3ii  10949
  Copyright terms: Public domain W3C validator