Theorem mp3an3 1363

Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)

Hypotheses

Ref	Expression
mp3an3.1	⊢ 𝜒
mp3an3.2	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mp3an3	⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Proof of Theorem mp3an3

Step	Hyp	Ref	Expression
1		mp3an3.1	. 2 ⊢ 𝜒
2		mp3an3.2	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	2	3expia 1232	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
4	1, 3	mpi 15	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  mp3an13  1365  mp3an23  1366  mp3anl3  1370  opelxp  4784  funimaexg  5445  ov  6181  ovmpoa  6192  ovmpo  6197  ovtposg  6503  oaword1  6717  th3q  6887  enrefg  7016  f1imaen  7047  mapxpen  7114  pw1fin  7183  xpfi  7205  djucomen  7536  addnnnq0  7780  mulnnnq0  7781  prarloclemcalc  7833  genpelxp  7842  genpprecll  7845  genppreclu  7846  addsrpr  8076  mulsrpr  8077  gt0srpr  8079  mulrid  8287  ltneg  8753  leneg  8756  suble0  8767  div1  8994  nnaddcl  9274  nnmulcl  9275  nnge1  9277  nnsub  9293  2halves  9484  halfaddsub  9489  addltmul  9492  fcdmnn0fsuppg  9568  zleltp1  9650  nnaddm1cl  9656  zextlt  9688  peano5uzti  9704  eluzp1p1  9898  uzaddcl  9936  znq  9974  xrre  10172  xrre2  10173  fzshftral  10464  nninfinf  10829  expn1ap0  10935  expadd  10967  expmul  10970  expubnd  10982  sqmul  10987  bernneq  11047  sqrecapd  11064  faclbnd2  11129  faclbnd6  11131  fihashssdif  11208  ccatlcan  11435  ccatrcan  11436  shftval3  11537  caucvgre  11691  leabs  11784  ltabs  11797  caubnd2  11827  efexp  12393  efival  12443  cos01gt0  12474  odd2np1  12584  halfleoddlt  12605  omoe  12607  opeo  12608  gcdmultiple  12741  sqgcd  12750  nn0seqcvgd  12763  phiprmpw  12944  eulerthlemth  12954  odzcllem  12965  pcelnn  13044  4sqlem3  13113  lsp0  14697  lss0v  14704  zndvds0  14924  ntrin  15115  txuni2  15247  txopn  15256  xblpnfps  15389  xblpnf  15390  bl2in  15394  unirnblps  15413  unirnbl  15414  blpnfctr  15430  plyconst  15736  plyid  15737  sincosq1eq  15830  rpcxpp1  15897  rplogb1  15939