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

Theorem pm3.2i 261
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 130 . 2  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
41, 2, 3mp2 16 1  |-  ( ph  /\ 
ps )
Colors of variables: wff set class
Syntax hints:    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 105
This theorem is referenced by:  mp4an  411  pm4.87  501  biijust  580  3pm3.2i  1093  sbequilem  1735  unssi  3145  ssini  3187  bm1.3ii  3905  epelg  4054  onsucelsucexmid  4282  elvv  4429  funpr  4978  mpt2v  5621  caovcom  5685  th3q  6241  endisj  6328  phplem2  6346  addnnnq0  6604  mulnnnq0  6605  nqprxx  6701  addsrpr  6887  mulsrpr  6888  recidpirq  6991  apreim  7667  mulcanapi  7721  div1  7753  recdivap  7768  divdivap1  7773  divdivap2  7774  divassapi  7818  divdirapi  7819  div23api  7820  div11api  7821  divmuldivapi  7822  divmul13api  7823  divadddivapi  7824  divdivdivapi  7825  lemulge11  7906  2cnne0  8190  2rene0  8191  1mhlfehlf  8199  halfpm6th  8201  2halves  8210  halfaddsub  8215  avglt1  8219  avglt2  8220  div4p1lem1div2  8234  3halfnz  8394  nneoor  8398  zeo  8401  divlt1lt  8747  divle1le  8748  nnledivrp  8783  2tnp1ge0ge0  9245  frecfzennn  9361  expge1  9451  faclbnd2  9603  4bc2eq6  9635  cjreb  9687  sqrt2gt1lt2  9868  amgm2  9937  3dvdsdec  10168  3dvds2dec  10169  odd2np1  10176  oddge22np1  10185  ltoddhalfle  10197  halfleoddlt  10198  nno  10210  ex-an  10249  ex-fl  10251  bdbm1.3ii  10370
  Copyright terms: Public domain W3C validator