Theorem mp3an3 1362

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

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1004

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 1006

This theorem is referenced by:  mp3an13  1364  mp3an23  1365  mp3anl3  1369  opelxp  4755  funimaexg  5414  ov  6141  ovmpoa  6152  ovmpo  6157  ovtposg  6425  oaword1  6639  th3q  6809  enrefg  6937  f1imaen  6968  mapxpen  7034  pw1fin  7102  xpfi  7124  djucomen  7431  addnnnq0  7669  mulnnnq0  7670  prarloclemcalc  7722  genpelxp  7731  genpprecll  7734  genppreclu  7735  addsrpr  7965  mulsrpr  7966  gt0srpr  7968  mulrid  8176  ltneg  8642  leneg  8645  suble0  8656  div1  8883  nnaddcl  9163  nnmulcl  9164  nnge1  9166  nnsub  9182  2halves  9373  halfaddsub  9378  addltmul  9381  zleltp1  9535  nnaddm1cl  9541  zextlt  9572  peano5uzti  9588  eluzp1p1  9782  uzaddcl  9820  znq  9858  xrre  10055  xrre2  10056  fzshftral  10343  nninfinf  10706  expn1ap0  10812  expadd  10844  expmul  10847  expubnd  10859  sqmul  10864  bernneq  10923  sqrecapd  10940  faclbnd2  11005  faclbnd6  11007  fihashssdif  11083  ccatlcan  11303  ccatrcan  11304  shftval3  11405  caucvgre  11559  leabs  11652  ltabs  11665  caubnd2  11695  efexp  12261  efival  12311  cos01gt0  12342  odd2np1  12452  halfleoddlt  12473  omoe  12475  opeo  12476  gcdmultiple  12609  sqgcd  12618  nn0seqcvgd  12631  phiprmpw  12812  eulerthlemth  12822  odzcllem  12833  pcelnn  12912  4sqlem3  12981  lsp0  14456  lss0v  14463  zndvds0  14683  ntrin  14867  txuni2  14999  txopn  15008  xblpnfps  15141  xblpnf  15142  bl2in  15146  unirnblps  15165  unirnbl  15166  blpnfctr  15182  plyconst  15488  plyid  15489  sincosq1eq  15582  rpcxpp1  15649  rplogb1  15691