NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  pm3.2i GIF version

Theorem pm3.2i 441
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 434 . 2 (φ → (ψ → (φ ψ)))
41, 2, 3mp2 17 1 (φ ψ)
Colors of variables: wff setvar class
Syntax hints:   wa 358
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 177  df-an 360
This theorem is referenced by:  pm4.87  567  dfbi  610  mp4an  654  3pm3.2i  1130  pm11.07  2115  unssi  3438  ssini  3478  elvvk  4207  ncfinraise  4481  evenoddnnnul  4514  brsi  4761  nfunv  5138  caovcom  5625  mpt2v  5719  op1st2nd  5790  fnfullfun  5858  bren  6030  endisj  6051  ce0addcnnul  6179
  Copyright terms: Public domain W3C validator