Theorem mp3an1 1443

Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)

Hypotheses

Ref	Expression
mp3an1.1	⊢ 𝜑
mp3an1.2	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mp3an1	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem mp3an1

Step	Hyp	Ref	Expression
1		mp3an1.1	. 2 ⊢ 𝜑
2		mp3an1.2	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	2	3expb 1115	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
4	1, 3	mpan 688	1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1082

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-an 399  df-3an 1084

This theorem is referenced by:  mp3an12  1446  mp3an1i  1449  mp3anl1  1450  mp3an  1456  mp3an2i  1461  mp3an3an  1462  onint  7503  wfrlem12  7959  tfrlem9  8014  oaord1  8170  oaword2  8172  oawordeulem  8173  oa00  8178  omword1  8192  omword2  8193  omlimcl  8197  oeoelem  8217  nnaordex  8257  enp1i  8746  dffi3  8888  unbnn3  9115  pwdjuen  9600  zorn2  9921  zornn0  9923  ttukey  9933  brdom7disj  9946  brdom6disj  9947  muladd11  10803  negsubdi  10935  mulneg1  11069  ltaddpos  11123  addge01  11143  reccl  11298  recid  11305  recid2  11306  recdiv2  11346  divdiv23zi  11386  ltmul12a  11489  lemul12a  11491  mulgt1  11492  ltmulgt11  11493  gt0div  11499  ge0div  11500  lediv12a  11526  ledivp1  11535  ltdiv23i  11557  ledivp1i  11558  ltdivp1i  11559  infm3  11593  8th4div3  11851  gtndiv  12053  nn0ind  12071  xrre2  12557  2resupmax  12575  qsqueeze  12588  xmulpnf1  12661  xlemul1a  12675  ioorebas  12833  elfz0ubfz0  13008  le2sq2  13497  expubnd  13538  crreczi  13586  bccl  13679  hashbc  13808  wrdred1hash  13908  ccatlid  13935  shftfval  14424  sgnp  14444  sqreulem  14714  binom1p  15181  fallrisefac  15374  efsub  15448  efi4p  15485  sinadd  15512  cosadd  15513  demoivreALT  15549  rpnnen2lem4  15565  odd2np1  15685  opoe  15707  omoe  15708  opeo  15709  omeo  15710  divalglem4  15742  divalglem9  15747  gcdcllem3  15845  gcdadd  15869  algcvgblem  15916  isprm3  16022  1arith2  16259  vdwap0  16307  vdwap1  16308  ipolt  17764  smndex1sgrp  18068  f1otrspeq  18570  rmodislmod  19697  mplsubrglem  20214  evls1rhm  20480  cnfldneg  20566  cnflddiv  20570  cnfldmulg  20572  cnfldexp  20573  zringmulg  20620  remulg  20746  resubgval  20748  thlleval  20837  frlmsslsp  20935  iccordt  21817  bl2ioo  23395  xrsblre  23414  iccntr  23424  icccmplem3  23427  reconnlem2  23430  opnreen  23434  iccpnfcnv  23543  cnllycmp  23555  pcoptcl  23620  ismbl2  24123  cmmbl  24130  nulmbl  24131  unmbl  24133  voliunlem2  24147  ioombl1  24158  opnmbllem  24197  mbfima  24226  ellimc3  24474  limcflf  24476  coe1termlem  24846  dvnply2  24874  dvnply  24875  reeff1o  25033  sinperlem  25064  resinf1o  25118  logeftb  25165  logge0  25186  efopn  25239  loglesqrt  25337  logrec  25339  xrlimcnp  25544  ppinncl  25749  chtrpcl  25750  bposlem2  25859  bposlem8  25865  lgsdir2  25904  1lgs  25914  ax5seglem2  26713  axcontlem2  26749  fusgrfis  27110  3cyclfrgrrn  28063  isgrpoi  28273  imsmetlem  28465  nmcvcn  28470  ipval2  28482  lnocoi  28532  nmlno0lem  28568  nmblolbii  28574  blometi  28578  blocnilem  28579  blocni  28580  ipasslem1  28606  ipasslem2  28607  ipasslem4  28609  ipasslem5  28610  ipasslem8  28612  ipblnfi  28630  ip2eqi  28631  ubthlem1  28645  htthlem  28692  h2hmetdval  28753  axhvcom-zf  28758  axhis1-zf  28769  axhis4-zf  28772  hvm1neg  28807  hvsub4  28812  hvsubass  28819  hvsubdistr2  28825  hv2times  28836  hvsubcan  28849  hvsubcan2  28850  his2sub  28867  norm-i  28904  normpyc  28921  hhip  28952  hhph  28953  norm1exi  29025  hhssabloilem  29036  hhssnv  29039  hhshsslem2  29043  hhssmetdval  29052  shscli  29092  shunssi  29143  shsleji  29145  shsidmi  29159  spanunsni  29354  h1datomi  29356  spansncvi  29427  pjss2i  29455  pjssmii  29456  pjocini  29473  homulid2  29575  honegdi  29584  ho2times  29594  nmopge0  29686  nmopgt0  29687  nmfnge0  29702  lnopaddi  29746  lnopmuli  29747  lnopsubi  29749  hmopbdoptHIL  29763  nmbdoplbi  29799  nmcoplbi  29803  nmophmi  29806  lnopconi  29809  lnfnaddi  29818  lnfnsubi  29821  nmbdfnlbi  29824  nmcfnlbi  29827  lnfnconi  29830  imaelshi  29833  cnlnadjlem2  29843  cnlnadjlem7  29848  nmoptrii  29869  nmopcoi  29870  adjcoi  29875  nmopcoadji  29876  bracnlnval  29889  leopmul  29909  opsqrlem1  29915  opsqrlem6  29920  hmopidmpji  29927  sto2i  30012  strlem1  30025  atcveq0  30123  atcv0eq  30154  atomli  30157  atcvati  30161  atcvat3i  30171  cdjreui  30207  cdj1i  30208  xdiv0  30605  xdivpnfrp  30609  mhmhmeotmd  31191  rezh  31233  qqhucn  31254  blsconn  32512  cnllysconn  32513  sate0fv0  32685  prv0  32698  sinccvglem  32936  nosupno  33224  nosupbday  33226  noetalem3  33240  opnrebl2  33690  ptrecube  34927  poimirlem6  34933  poimirlem7  34934  poimirlem29  34956  poimirlem30  34957  opnmbllem0  34963  mblfinlem3  34966  mblfinlem4  34967  ismblfin  34968  voliunnfl  34971  ftc1anclem5  35004  ftc1anclem7  35006  ftc1anclem8  35007  ftc1anc  35008  heiborlem7  35128  rrnequiv  35146  ismrer1  35149  el3v1  35525  cnaddcom  36141  lcmineqlem1  39157  2xp3dxp2ge1d  39173  sn-ltaddpos  39319  mapco2  39388  mzpaddmpt  39414  mzpmulmpt  39415  zindbi  39619  mpaaeu  39826  eel000cT  41111  eel0TT  41112  supminfxr  41814  fmtno4prmfac  43808  zringsubgval  44523  aacllem  44976