Theorem mp3an3 1367

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  mp3an13  1369  mp3an23  1370  mp3anl3  1374  opelxp  4804  funimaexg  5465  ov  6208  ovmpoa  6219  ovmpo  6224  ovtposg  6530  oaword1  6744  th3q  6914  enrefg  7050  f1imaen  7081  mapxpen  7148  pw1fin  7217  xpfi  7239  djucomen  7573  addnnnq0  7817  mulnnnq0  7818  prarloclemcalc  7870  genpelxp  7879  genpprecll  7882  genppreclu  7883  addsrpr  8113  mulsrpr  8114  gt0srpr  8116  mulrid  8324  ltneg  8792  leneg  8795  suble0  8806  div1  9036  nnaddcl  9327  nnmulcl  9328  nnge1  9330  nnsub  9346  2halves  9539  halfaddsub  9544  addltmul  9547  fcdmnn0fsuppg  9623  zleltp1  9705  nnaddm1cl  9711  zextlt  9743  peano5uzti  9759  eluzp1p1  9958  uzaddcl  9996  znq  10034  xrre  10233  xrre2  10234  fzshftral  10526  nninfinf  10895  expn1ap0  11001  expadd  11033  expmul  11036  expubnd  11048  sqmul  11053  bernneq  11113  sqrecapd  11130  faclbnd2  11196  faclbnd6  11198  fihashssdif  11275  ccatlcan  11506  ccatrcan  11507  shftval3  11608  caucvgre  11763  leabs  11856  ltabs  11870  caubnd2  11900  efexp  12468  efival  12518  cos01gt0  12549  odd2np1  12659  halfleoddlt  12680  omoe  12682  opeo  12683  gcdmultiple  12816  sqgcd  12825  nn0seqcvgd  12838  phiprmpw  13023  eulerthlemth  13033  odzcllem  13044  pcelnn  13123  4sqlem3  13192  lsp0  14844  lss0v  14851  zndvds0  15069  ntrin  15316  txuni2  15448  txopn  15457  xblpnfps  15590  xblpnf  15591  bl2in  15595  unirnblps  15614  unirnbl  15615  blpnfctr  15631  plyconst  15937  plyid  15938  sincosq1eq  16032  rpcxpp1  16103  rplogb1  16145  ppiqub  16254  bposlem1  16272  bposlem2  16273  bposlem9  16280