Theorem mp3an1 1471

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1099

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 400  df-3an 1101

This theorem is referenced by:  mp3an12  1474  mp3an1i  1477  mp3anl1  1478  mp3an  1484  mp3an2i  1489  mp3an3an  1490  onint  7775  tfrlem9  8358  oaord1  8522  oaword2  8524  oawordeulem  8525  oa00  8530  omword1  8544  omword2  8545  omlimcl  8549  oeoelem  8570  nnaordex  8610  naddword1  8664  undom  9039  sucdom2  9173  fodomfi  9258  fodomfib  9275  dffi3  9379  unbnn3  9616  ttrcltr  9673  frmin  9709  frrlem16  9718  pwdjuen  10140  zorn2  10465  zornn0  10467  ttukey  10477  brdom7disj  10490  brdom6disj  10491  muladd11  11355  negsubdi  11489  mulneg1  11625  ltaddpos  11679  addge01  11699  reccl  11854  recid  11861  recid2  11862  div0  11880  recdiv2  11906  divdiv23zi  11946  ltmul12a  12049  lemul12a  12051  mulgt1OLD  12052  ltmulgt11  12053  gt0div  12060  ge0div  12061  lediv12a  12087  ledivp1  12096  ltdiv23i  12118  ledivp1i  12119  ltdivp1i  12120  infm3  12153  8th4div3  12443  gtndiv  12652  nn0ind  12670  xrre2  13175  2resupmax  13193  qsqueeze  13206  xmulpnf1  13279  xlemul1a  13293  ioorebas  13457  elfz0ubfz0  13639  le2sq2  14150  expubnd  14193  crreczi  14243  bccl  14337  hashbc  14468  wrdred1hash  14576  ccatlid  14602  shftfval  15085  sgnp  15105  sqreulem  15389  binom1p  15863  fallrisefac  16057  efsub  16134  efi4p  16171  sinadd  16198  cosadd  16199  demoivreALT  16235  rpnnen2lem4  16251  odd2np1  16377  opoe  16399  omoe  16400  opeo  16401  omeo  16402  divalglem4  16432  divalglem9  16437  gcdcllem3  16537  gcdadd  16562  algcvgblem  16613  isprm3  16719  1arith2  16966  vdwap0  17014  vdwap1  17015  ipolt  18569  smndex1sgrp  18947  f1otrspeq  19489  rmodislmod  20999  cnfldneg  21452  cnflddiv  21456  cnfldmulg  21458  cnfldexp  21459  zringsub  21509  zringmulg  21510  zringsubgval  21524  remulg  21661  resubgval  21663  thlleval  21752  mplsubrglem  22057  evls1rhm  22387  iccordt  23276  bl2ioo  24854  xrsblre  24874  iccntr  24884  icccmplem3  24887  reconnlem2  24890  opnreen  24894  mpomulcn  24931  iccpnfcnv  25008  cnllycmp  25020  pcoptcl  25085  ismbl2  25591  cmmbl  25598  nulmbl  25599  unmbl  25601  voliunlem2  25615  ioombl1  25626  opnmbllem  25665  mbfima  25694  ellimc3  25943  limcflf  25945  coe1termlem  26320  dvnply2  26353  dvnply  26354  reeff1o  26512  sinperlem  26547  resinf1o  26603  logeftb  26650  logge0  26672  efopn  26725  loglesqrt  26828  logrec  26830  xrlimcnp  27035  ppinncl  27240  chtrpcl  27241  bposlem2  27351  bposlem8  27357  lgsdir2  27396  1lgs  27406  nosupno  27769  nosupbday  27771  noinfno  27784  noinfbday  27786  noetasuplem4  27802  lrrecfr  28038  ltmuls  28231  bdayfinbndlem1  28562  ax5seglem2  29132  axcontlem2  29168  fusgrfis  29533  3cyclfrgrrn  30490  isgrpoi  30703  imsmetlem  30895  nmcvcn  30900  ipval2  30912  lnocoi  30962  nmlno0lem  30998  nmblolbii  31004  blometi  31008  blocnilem  31009  blocni  31010  ipasslem1  31036  ipasslem2  31037  ipasslem4  31039  ipasslem5  31040  ipasslem8  31042  ipblnfi  31060  ip2eqi  31061  ubthlem1  31075  htthlem  31122  h2hmetdval  31183  axhvcom-zf  31188  axhis1-zf  31199  axhis4-zf  31202  hvm1neg  31237  hvsub4  31242  hvsubass  31249  hvsubdistr2  31255  hv2times  31266  hvsubcan  31279  hvsubcan2  31280  his2sub  31297  norm-i  31334  normpyc  31351  hhip  31382  hhph  31383  norm1exi  31455  hhssabloilem  31466  hhssnv  31469  hhshsslem2  31473  hhssmetdval  31482  shscli  31522  shunssi  31573  shsleji  31575  shsidmi  31589  spanunsni  31784  h1datomi  31786  spansncvi  31857  pjss2i  31885  pjssmii  31886  pjocini  31903  homullid  32005  honegdi  32014  ho2times  32024  nmopge0  32116  nmopgt0  32117  nmfnge0  32132  lnopaddi  32176  lnopmuli  32177  lnopsubi  32179  hmopbdoptHIL  32193  nmbdoplbi  32229  nmcoplbi  32233  nmophmi  32236  lnopconi  32239  lnfnaddi  32248  lnfnsubi  32251  nmbdfnlbi  32254  nmcfnlbi  32257  lnfnconi  32260  imaelshi  32263  cnlnadjlem2  32273  cnlnadjlem7  32278  nmoptrii  32299  nmopcoi  32300  adjcoi  32305  nmopcoadji  32306  bracnlnval  32319  leopmul  32339  opsqrlem1  32345  opsqrlem6  32350  hmopidmpji  32357  sto2i  32442  strlem1  32455  atcveq0  32553  atcv0eq  32584  atomli  32587  atcvati  32591  atcvat3i  32601  cdjreui  32637  cdj1i  32638  xdiv0  33108  xdivpnfrp  33112  mhmhmeotmd  34226  rezh  34268  qqhucn  34291  blsconn  35599  cnllysconn  35600  sate0fv0  35772  prv0  35785  sinccvglem  36027  opnrebl2  36686  ptrecube  38124  poimirlem6  38130  poimirlem7  38131  poimirlem29  38153  poimirlem30  38154  opnmbllem0  38160  mblfinlem3  38163  mblfinlem4  38164  ismblfin  38165  voliunnfl  38168  ftc1anclem5  38201  ftc1anclem7  38203  ftc1anclem8  38204  ftc1anc  38205  heiborlem7  38321  rrnequiv  38339  ismrer1  38342  el3v1  38734  preuniqval  39000  cnaddcom  39601  lcmineqlem1  42651  sn-ltaddpos  43080  mapco2  43301  mzpaddmpt  43327  mzpmulmpt  43328  zindbi  43528  mpaaeu  43732  tfsconcat0b  43928  eel000cT  45283  eel0TT  45284  supminfxr  46043  fmtno4prmfac  48186  pgn4cyclex  48753  aacllem  50427