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  4779  funimaexg  5440  ov  6173  ovmpoa  6184  ovmpo  6189  ovtposg  6490  oaword1  6704  th3q  6874  enrefg  7003  f1imaen  7034  mapxpen  7101  pw1fin  7170  xpfi  7192  djucomen  7523  addnnnq0  7764  mulnnnq0  7765  prarloclemcalc  7817  genpelxp  7826  genpprecll  7829  genppreclu  7830  addsrpr  8060  mulsrpr  8061  gt0srpr  8063  mulrid  8271  ltneg  8736  leneg  8739  suble0  8750  div1  8977  nnaddcl  9257  nnmulcl  9258  nnge1  9260  nnsub  9276  2halves  9467  halfaddsub  9472  addltmul  9475  fcdmnn0fsuppg  9551  zleltp1  9633  nnaddm1cl  9639  zextlt  9670  peano5uzti  9686  eluzp1p1  9880  uzaddcl  9918  znq  9956  xrre  10153  xrre2  10154  fzshftral  10442  nninfinf  10805  expn1ap0  10911  expadd  10943  expmul  10946  expubnd  10958  sqmul  10963  bernneq  11022  sqrecapd  11039  faclbnd2  11104  faclbnd6  11106  fihashssdif  11183  ccatlcan  11410  ccatrcan  11411  shftval3  11512  caucvgre  11666  leabs  11759  ltabs  11772  caubnd2  11802  efexp  12368  efival  12418  cos01gt0  12449  odd2np1  12559  halfleoddlt  12580  omoe  12582  opeo  12583  gcdmultiple  12716  sqgcd  12725  nn0seqcvgd  12738  phiprmpw  12919  eulerthlemth  12929  odzcllem  12940  pcelnn  13019  4sqlem3  13088  lsp0  14571  lss0v  14578  zndvds0  14798  ntrin  14989  txuni2  15121  txopn  15130  xblpnfps  15263  xblpnf  15264  bl2in  15268  unirnblps  15287  unirnbl  15288  blpnfctr  15304  plyconst  15610  plyid  15611  sincosq1eq  15704  rpcxpp1  15771  rplogb1  15813