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  6140  ovmpoa  6151  ovmpo  6156  ovtposg  6424  oaword1  6638  th3q  6808  enrefg  6936  f1imaen  6967  mapxpen  7033  pw1fin  7101  xpfi  7123  djucomen  7430  addnnnq0  7668  mulnnnq0  7669  prarloclemcalc  7721  genpelxp  7730  genpprecll  7733  genppreclu  7734  addsrpr  7964  mulsrpr  7965  gt0srpr  7967  mulrid  8175  ltneg  8641  leneg  8644  suble0  8655  div1  8882  nnaddcl  9162  nnmulcl  9163  nnge1  9165  nnsub  9181  2halves  9372  halfaddsub  9377  addltmul  9380  zleltp1  9534  nnaddm1cl  9540  zextlt  9571  peano5uzti  9587  eluzp1p1  9781  uzaddcl  9819  znq  9857  xrre  10054  xrre2  10055  fzshftral  10342  nninfinf  10704  expn1ap0  10810  expadd  10842  expmul  10845  expubnd  10857  sqmul  10862  bernneq  10921  sqrecapd  10938  faclbnd2  11003  faclbnd6  11005  fihashssdif  11081  ccatlcan  11298  ccatrcan  11299  shftval3  11387  caucvgre  11541  leabs  11634  ltabs  11647  caubnd2  11677  efexp  12242  efival  12292  cos01gt0  12323  odd2np1  12433  halfleoddlt  12454  omoe  12456  opeo  12457  gcdmultiple  12590  sqgcd  12599  nn0seqcvgd  12612  phiprmpw  12793  eulerthlemth  12803  odzcllem  12814  pcelnn  12893  4sqlem3  12962  lsp0  14436  lss0v  14443  zndvds0  14663  ntrin  14847  txuni2  14979  txopn  14988  xblpnfps  15121  xblpnf  15122  bl2in  15126  unirnblps  15145  unirnbl  15146  blpnfctr  15162  plyconst  15468  plyid  15469  sincosq1eq  15562  rpcxpp1  15629  rplogb1  15671