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  7083  xpfi  7105  djucomen  7409  addnnnq0  7647  mulnnnq0  7648  prarloclemcalc  7700  genpelxp  7709  genpprecll  7712  genppreclu  7713  addsrpr  7943  mulsrpr  7944  gt0srpr  7946  mulrid  8154  ltneg  8620  leneg  8623  suble0  8634  div1  8861  nnaddcl  9141  nnmulcl  9142  nnge1  9144  nnsub  9160  2halves  9351  halfaddsub  9356  addltmul  9359  zleltp1  9513  nnaddm1cl  9519  zextlt  9550  peano5uzti  9566  eluzp1p1  9760  uzaddcl  9793  znq  9831  xrre  10028  xrre2  10029  fzshftral  10316  nninfinf  10677  expn1ap0  10783  expadd  10815  expmul  10818  expubnd  10830  sqmul  10835  bernneq  10894  sqrecapd  10911  faclbnd2  10976  faclbnd6  10978  fihashssdif  11053  ccatlcan  11266  ccatrcan  11267  shftval3  11354  caucvgre  11508  leabs  11601  ltabs  11614  caubnd2  11644  efexp  12209  efival  12259  cos01gt0  12290  odd2np1  12400  halfleoddlt  12421  omoe  12423  opeo  12424  gcdmultiple  12557  sqgcd  12566  nn0seqcvgd  12579  phiprmpw  12760  eulerthlemth  12770  odzcllem  12781  pcelnn  12860  4sqlem3  12929  lsp0  14403  lss0v  14410  zndvds0  14630  ntrin  14814  txuni2  14946  txopn  14955  xblpnfps  15088  xblpnf  15089  bl2in  15093  unirnblps  15112  unirnbl  15113  blpnfctr  15129  plyconst  15435  plyid  15436  sincosq1eq  15529  rpcxpp1  15596  rplogb1  15638