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  4753  funimaexg  5411  ov  6136  ovmpoa  6147  ovmpo  6152  ovtposg  6420  oaword1  6634  th3q  6804  enrefg  6932  f1imaen  6963  mapxpen  7029  pw1fin  7095  xpfi  7117  djucomen  7421  addnnnq0  7659  mulnnnq0  7660  prarloclemcalc  7712  genpelxp  7721  genpprecll  7724  genppreclu  7725  addsrpr  7955  mulsrpr  7956  gt0srpr  7958  mulrid  8166  ltneg  8632  leneg  8635  suble0  8646  div1  8873  nnaddcl  9153  nnmulcl  9154  nnge1  9156  nnsub  9172  2halves  9363  halfaddsub  9368  addltmul  9371  zleltp1  9525  nnaddm1cl  9531  zextlt  9562  peano5uzti  9578  eluzp1p1  9772  uzaddcl  9810  znq  9848  xrre  10045  xrre2  10046  fzshftral  10333  nninfinf  10695  expn1ap0  10801  expadd  10833  expmul  10836  expubnd  10848  sqmul  10853  bernneq  10912  sqrecapd  10929  faclbnd2  10994  faclbnd6  10996  fihashssdif  11072  ccatlcan  11289  ccatrcan  11290  shftval3  11378  caucvgre  11532  leabs  11625  ltabs  11638  caubnd2  11668  efexp  12233  efival  12283  cos01gt0  12314  odd2np1  12424  halfleoddlt  12445  omoe  12447  opeo  12448  gcdmultiple  12581  sqgcd  12590  nn0seqcvgd  12603  phiprmpw  12784  eulerthlemth  12794  odzcllem  12805  pcelnn  12884  4sqlem3  12953  lsp0  14427  lss0v  14434  zndvds0  14654  ntrin  14838  txuni2  14970  txopn  14979  xblpnfps  15112  xblpnf  15113  bl2in  15117  unirnblps  15136  unirnbl  15137  blpnfctr  15153  plyconst  15459  plyid  15460  sincosq1eq  15553  rpcxpp1  15620  rplogb1  15662