Theorem mp3an3 1316

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

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 968

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

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  mp3an13  1318  mp3an23  1319  mp3anl3  1323  opelxp  4634  funimaexg  5272  ov  5961  ovmpoa  5972  ovmpo  5977  ovtposg  6227  oaword1  6439  th3q  6606  enrefg  6730  f1imaen  6760  mapxpen  6814  pw1fin  6876  xpfi  6895  djucomen  7172  addnnnq0  7390  mulnnnq0  7391  prarloclemcalc  7443  genpelxp  7452  genpprecll  7455  genppreclu  7456  addsrpr  7686  mulsrpr  7687  gt0srpr  7689  mulid1  7896  ltneg  8360  leneg  8363  suble0  8374  div1  8599  nnaddcl  8877  nnmulcl  8878  nnge1  8880  nnsub  8896  2halves  9086  halfaddsub  9091  addltmul  9093  zleltp1  9246  nnaddm1cl  9252  zextlt  9283  peano5uzti  9299  eluzp1p1  9491  uzaddcl  9524  znq  9562  xrre  9756  xrre2  9757  fzshftral  10043  expn1ap0  10465  expadd  10497  expmul  10500  expubnd  10512  sqmul  10517  bernneq  10575  sqrecapd  10592  faclbnd2  10655  faclbnd6  10657  fihashssdif  10731  shftval3  10769  caucvgre  10923  leabs  11016  ltabs  11029  caubnd2  11059  efexp  11623  efival  11673  cos01gt0  11703  odd2np1  11810  halfleoddlt  11831  omoe  11833  opeo  11834  gcdmultiple  11953  sqgcd  11962  nn0seqcvgd  11973  phiprmpw  12154  eulerthlemth  12164  odzcllem  12174  pcelnn  12252  4sqlem3  12320  ntrin  12764  txuni2  12896  txopn  12905  xblpnfps  13038  xblpnf  13039  bl2in  13043  unirnblps  13062  unirnbl  13063  blpnfctr  13079  sincosq1eq  13400  rpcxpp1  13467  rplogb1  13506