Theorem mp3an1 1451

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 1121	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
4	1, 3	mpan 691	1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  mp3an12  1454  mp3an1i  1457  mp3anl1  1458  mp3an  1464  mp3an2i  1469  mp3an3an  1470  onint  7735  tfrlem9  8316  oaord1  8478  oaword2  8480  oawordeulem  8481  oa00  8486  omword1  8500  omword2  8501  omlimcl  8505  oeoelem  8526  nnaordex  8566  naddword1  8619  undom  8995  sucdom2  9129  fodomfi  9214  fodomfib  9231  dffi3  9336  unbnn3  9570  ttrcltr  9627  frmin  9663  frrlem16  9672  pwdjuen  10094  zorn2  10418  zornn0  10420  ttukey  10430  brdom7disj  10443  brdom6disj  10444  muladd11  11305  negsubdi  11439  mulneg1  11575  ltaddpos  11629  addge01  11649  reccl  11805  recid  11812  recid2  11813  div0  11831  recdiv2  11856  divdiv23zi  11896  ltmul12a  11999  lemul12a  12001  mulgt1OLD  12002  ltmulgt11  12003  gt0div  12010  ge0div  12011  lediv12a  12037  ledivp1  12046  ltdiv23i  12068  ledivp1i  12069  ltdivp1i  12070  infm3  12103  8th4div3  12363  gtndiv  12571  nn0ind  12589  xrre2  13087  2resupmax  13105  qsqueeze  13118  xmulpnf1  13191  xlemul1a  13205  ioorebas  13369  elfz0ubfz0  13550  le2sq2  14060  expubnd  14103  crreczi  14153  bccl  14247  hashbc  14378  wrdred1hash  14486  ccatlid  14512  shftfval  14995  sgnp  15015  sqreulem  15285  binom1p  15756  fallrisefac  15950  efsub  16027  efi4p  16064  sinadd  16091  cosadd  16092  demoivreALT  16128  rpnnen2lem4  16144  odd2np1  16270  opoe  16292  omoe  16293  opeo  16294  omeo  16295  divalglem4  16325  divalglem9  16330  gcdcllem3  16430  gcdadd  16455  algcvgblem  16506  isprm3  16612  1arith2  16858  vdwap0  16906  vdwap1  16907  ipolt  18460  smndex1sgrp  18835  f1otrspeq  19378  rmodislmod  20883  cnfldneg  21352  cnflddiv  21357  cnflddivOLD  21358  cnfldmulg  21360  cnfldexp  21361  zringsub  21412  zringmulg  21413  zringsubgval  21427  remulg  21564  resubgval  21566  thlleval  21655  mplsubrglem  21961  evls1rhm  22268  iccordt  23160  bl2ioo  24738  xrsblre  24758  iccntr  24768  icccmplem3  24771  reconnlem2  24774  opnreen  24778  mpomulcn  24816  iccpnfcnv  24900  cnllycmp  24913  pcoptcl  24979  ismbl2  25486  cmmbl  25493  nulmbl  25494  unmbl  25496  voliunlem2  25510  ioombl1  25521  opnmbllem  25560  mbfima  25589  ellimc3  25838  limcflf  25840  coe1termlem  26221  dvnply2  26253  dvnply  26254  reeff1o  26415  sinperlem  26447  resinf1o  26503  logeftb  26550  logge0  26572  efopn  26625  loglesqrt  26729  logrec  26731  xrlimcnp  26936  ppinncl  27142  chtrpcl  27143  bposlem2  27254  bposlem8  27260  lgsdir2  27299  1lgs  27309  nosupno  27673  nosupbday  27675  noinfno  27688  noinfbday  27690  noetasuplem4  27706  lrrecfr  27923  sltmul  28116  bdayfinbndlem1  28444  ax5seglem2  28983  axcontlem2  29019  fusgrfis  29384  3cyclfrgrrn  30342  isgrpoi  30554  imsmetlem  30746  nmcvcn  30751  ipval2  30763  lnocoi  30813  nmlno0lem  30849  nmblolbii  30855  blometi  30859  blocnilem  30860  blocni  30861  ipasslem1  30887  ipasslem2  30888  ipasslem4  30890  ipasslem5  30891  ipasslem8  30893  ipblnfi  30911  ip2eqi  30912  ubthlem1  30926  htthlem  30973  h2hmetdval  31034  axhvcom-zf  31039  axhis1-zf  31050  axhis4-zf  31053  hvm1neg  31088  hvsub4  31093  hvsubass  31100  hvsubdistr2  31106  hv2times  31117  hvsubcan  31130  hvsubcan2  31131  his2sub  31148  norm-i  31185  normpyc  31202  hhip  31233  hhph  31234  norm1exi  31306  hhssabloilem  31317  hhssnv  31320  hhshsslem2  31324  hhssmetdval  31333  shscli  31373  shunssi  31424  shsleji  31426  shsidmi  31440  spanunsni  31635  h1datomi  31637  spansncvi  31708  pjss2i  31736  pjssmii  31737  pjocini  31754  homullid  31856  honegdi  31865  ho2times  31875  nmopge0  31967  nmopgt0  31968  nmfnge0  31983  lnopaddi  32027  lnopmuli  32028  lnopsubi  32030  hmopbdoptHIL  32044  nmbdoplbi  32080  nmcoplbi  32084  nmophmi  32087  lnopconi  32090  lnfnaddi  32099  lnfnsubi  32102  nmbdfnlbi  32105  nmcfnlbi  32108  lnfnconi  32111  imaelshi  32114  cnlnadjlem2  32124  cnlnadjlem7  32129  nmoptrii  32150  nmopcoi  32151  adjcoi  32156  nmopcoadji  32157  bracnlnval  32170  leopmul  32190  opsqrlem1  32196  opsqrlem6  32201  hmopidmpji  32208  sto2i  32293  strlem1  32306  atcveq0  32404  atcv0eq  32435  atomli  32438  atcvati  32442  atcvat3i  32452  cdjreui  32488  cdj1i  32489  xdiv0  32989  xdivpnfrp  32993  mhmhmeotmd  34063  rezh  34105  qqhucn  34128  blsconn  35417  cnllysconn  35418  sate0fv0  35590  prv0  35603  sinccvglem  35845  opnrebl2  36494  ptrecube  37790  poimirlem6  37796  poimirlem7  37797  poimirlem29  37819  poimirlem30  37820  opnmbllem0  37826  mblfinlem3  37829  mblfinlem4  37830  ismblfin  37831  voliunnfl  37834  ftc1anclem5  37867  ftc1anclem7  37869  ftc1anclem8  37870  ftc1anc  37871  heiborlem7  37987  rrnequiv  38005  ismrer1  38008  el3v1  38400  preuniqval  38666  cnaddcom  39267  lcmineqlem1  42318  sn-ltaddpos  42745  mapco2  42994  mzpaddmpt  43020  mzpmulmpt  43021  zindbi  43225  mpaaeu  43429  tfsconcat0b  43625  eel000cT  44980  eel0TT  44981  supminfxr  45745  fmtno4prmfac  47855  pgn4cyclex  48409  aacllem  50083