Theorem mp3an3 1360

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 1229	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
4	1, 3	mpi 15	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

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

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 1004

This theorem is referenced by:  mp3an13  1362  mp3an23  1363  mp3anl3  1367  opelxp  4749  funimaexg  5405  ov  6130  ovmpoa  6141  ovmpo  6146  ovtposg  6411  oaword1  6625  th3q  6795  enrefg  6923  f1imaen  6954  mapxpen  7017  pw1fin  7080  xpfi  7102  djucomen  7406  addnnnq0  7644  mulnnnq0  7645  prarloclemcalc  7697  genpelxp  7706  genpprecll  7709  genppreclu  7710  addsrpr  7940  mulsrpr  7941  gt0srpr  7943  mulrid  8151  ltneg  8617  leneg  8620  suble0  8631  div1  8858  nnaddcl  9138  nnmulcl  9139  nnge1  9141  nnsub  9157  2halves  9348  halfaddsub  9353  addltmul  9356  zleltp1  9510  nnaddm1cl  9516  zextlt  9547  peano5uzti  9563  eluzp1p1  9756  uzaddcl  9789  znq  9827  xrre  10024  xrre2  10025  fzshftral  10312  nninfinf  10673  expn1ap0  10779  expadd  10811  expmul  10814  expubnd  10826  sqmul  10831  bernneq  10890  sqrecapd  10907  faclbnd2  10972  faclbnd6  10974  fihashssdif  11048  ccatlcan  11258  ccatrcan  11259  shftval3  11346  caucvgre  11500  leabs  11593  ltabs  11606  caubnd2  11636  efexp  12201  efival  12251  cos01gt0  12282  odd2np1  12392  halfleoddlt  12413  omoe  12415  opeo  12416  gcdmultiple  12549  sqgcd  12558  nn0seqcvgd  12571  phiprmpw  12752  eulerthlemth  12762  odzcllem  12773  pcelnn  12852  4sqlem3  12921  lsp0  14395  lss0v  14402  zndvds0  14622  ntrin  14806  txuni2  14938  txopn  14947  xblpnfps  15080  xblpnf  15081  bl2in  15085  unirnblps  15104  unirnbl  15105  blpnfctr  15121  plyconst  15427  plyid  15428  sincosq1eq  15521  rpcxpp1  15588  rplogb1  15630