Theorem mp3an3 1315

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

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

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 969

This theorem is referenced by:  mp3an13  1317  mp3an23  1318  mp3anl3  1322  opelxp  4628  funimaexg  5266  ov  5952  ovmpoa  5963  ovmpo  5968  ovtposg  6218  oaword1  6430  th3q  6597  enrefg  6721  f1imaen  6751  mapxpen  6805  pw1fin  6867  xpfi  6886  djucomen  7163  addnnnq0  7381  mulnnnq0  7382  prarloclemcalc  7434  genpelxp  7443  genpprecll  7446  genppreclu  7447  addsrpr  7677  mulsrpr  7678  gt0srpr  7680  mulid1  7887  ltneg  8351  leneg  8354  suble0  8365  div1  8590  nnaddcl  8868  nnmulcl  8869  nnge1  8871  nnsub  8887  2halves  9077  halfaddsub  9082  addltmul  9084  zleltp1  9237  nnaddm1cl  9243  zextlt  9274  peano5uzti  9290  eluzp1p1  9482  uzaddcl  9515  znq  9553  xrre  9747  xrre2  9748  fzshftral  10033  expn1ap0  10455  expadd  10487  expmul  10490  expubnd  10502  sqmul  10507  bernneq  10564  sqrecapd  10581  faclbnd2  10644  faclbnd6  10646  fihashssdif  10720  shftval3  10755  caucvgre  10909  leabs  11002  ltabs  11015  caubnd2  11045  efexp  11609  efival  11659  cos01gt0  11689  odd2np1  11795  halfleoddlt  11816  omoe  11818  opeo  11819  gcdmultiple  11938  sqgcd  11947  nn0seqcvgd  11952  phiprmpw  12131  eulerthlemth  12141  odzcllem  12151  pcelnn  12229  ntrin  12665  txuni2  12797  txopn  12806  xblpnfps  12939  xblpnf  12940  bl2in  12944  unirnblps  12963  unirnbl  12964  blpnfctr  12980  sincosq1eq  13301  rpcxpp1  13368  rplogb1  13407