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  4761  funimaexg  5421  ov  6151  ovmpoa  6162  ovmpo  6167  ovtposg  6468  oaword1  6682  th3q  6852  enrefg  6980  f1imaen  7011  mapxpen  7077  pw1fin  7145  xpfi  7167  djucomen  7491  addnnnq0  7729  mulnnnq0  7730  prarloclemcalc  7782  genpelxp  7791  genpprecll  7794  genppreclu  7795  addsrpr  8025  mulsrpr  8026  gt0srpr  8028  mulrid  8236  ltneg  8701  leneg  8704  suble0  8715  div1  8942  nnaddcl  9222  nnmulcl  9223  nnge1  9225  nnsub  9241  2halves  9432  halfaddsub  9437  addltmul  9440  zleltp1  9596  nnaddm1cl  9602  zextlt  9633  peano5uzti  9649  eluzp1p1  9843  uzaddcl  9881  znq  9919  xrre  10116  xrre2  10117  fzshftral  10405  nninfinf  10768  expn1ap0  10874  expadd  10906  expmul  10909  expubnd  10921  sqmul  10926  bernneq  10985  sqrecapd  11002  faclbnd2  11067  faclbnd6  11069  fihashssdif  11145  ccatlcan  11365  ccatrcan  11366  shftval3  11467  caucvgre  11621  leabs  11714  ltabs  11727  caubnd2  11757  efexp  12323  efival  12373  cos01gt0  12404  odd2np1  12514  halfleoddlt  12535  omoe  12537  opeo  12538  gcdmultiple  12671  sqgcd  12680  nn0seqcvgd  12693  phiprmpw  12874  eulerthlemth  12884  odzcllem  12895  pcelnn  12974  4sqlem3  13043  lsp0  14519  lss0v  14526  zndvds0  14746  ntrin  14935  txuni2  15067  txopn  15076  xblpnfps  15209  xblpnf  15210  bl2in  15214  unirnblps  15233  unirnbl  15234  blpnfctr  15250  plyconst  15556  plyid  15557  sincosq1eq  15650  rpcxpp1  15717  rplogb1  15759