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  7741  tfrlem9  8321  oaord1  8483  oaword2  8485  oawordeulem  8486  oa00  8491  omword1  8505  omword2  8506  omlimcl  8510  oeoelem  8531  nnaordex  8571  naddword1  8624  undom  9000  sucdom2  9134  fodomfi  9219  fodomfib  9236  dffi3  9341  unbnn3  9577  ttrcltr  9634  frmin  9670  frrlem16  9679  pwdjuen  10101  zorn2  10425  zornn0  10427  ttukey  10437  brdom7disj  10450  brdom6disj  10451  muladd11  11313  negsubdi  11447  mulneg1  11583  ltaddpos  11637  addge01  11657  reccl  11813  recid  11820  recid2  11821  div0  11839  recdiv2  11865  divdiv23zi  11905  ltmul12a  12008  lemul12a  12010  mulgt1OLD  12011  ltmulgt11  12012  gt0div  12019  ge0div  12020  lediv12a  12046  ledivp1  12055  ltdiv23i  12077  ledivp1i  12078  ltdivp1i  12079  infm3  12112  8th4div3  12394  gtndiv  12603  nn0ind  12621  xrre2  13119  2resupmax  13137  qsqueeze  13150  xmulpnf1  13223  xlemul1a  13237  ioorebas  13401  elfz0ubfz0  13583  le2sq2  14094  expubnd  14137  crreczi  14187  bccl  14281  hashbc  14412  wrdred1hash  14520  ccatlid  14546  shftfval  15029  sgnp  15049  sqreulem  15319  binom1p  15793  fallrisefac  15987  efsub  16064  efi4p  16101  sinadd  16128  cosadd  16129  demoivreALT  16165  rpnnen2lem4  16181  odd2np1  16307  opoe  16329  omoe  16330  opeo  16331  omeo  16332  divalglem4  16362  divalglem9  16367  gcdcllem3  16467  gcdadd  16492  algcvgblem  16543  isprm3  16649  1arith2  16896  vdwap0  16944  vdwap1  16945  ipolt  18498  smndex1sgrp  18876  f1otrspeq  19419  rmodislmod  20922  cnfldneg  21391  cnflddiv  21396  cnflddivOLD  21397  cnfldmulg  21399  cnfldexp  21400  zringsub  21451  zringmulg  21452  zringsubgval  21466  remulg  21603  resubgval  21605  thlleval  21694  mplsubrglem  21998  evls1rhm  22303  iccordt  23195  bl2ioo  24773  xrsblre  24793  iccntr  24803  icccmplem3  24806  reconnlem2  24809  opnreen  24813  mpomulcn  24850  iccpnfcnv  24927  cnllycmp  24939  pcoptcl  25004  ismbl2  25510  cmmbl  25517  nulmbl  25518  unmbl  25520  voliunlem2  25534  ioombl1  25545  opnmbllem  25584  mbfima  25613  ellimc3  25862  limcflf  25864  coe1termlem  26239  dvnply2  26270  dvnply  26271  reeff1o  26431  sinperlem  26463  resinf1o  26519  logeftb  26566  logge0  26588  efopn  26641  loglesqrt  26744  logrec  26746  xrlimcnp  26951  ppinncl  27157  chtrpcl  27158  bposlem2  27268  bposlem8  27274  lgsdir2  27313  1lgs  27323  nosupno  27687  nosupbday  27689  noinfno  27702  noinfbday  27704  noetasuplem4  27720  lrrecfr  27955  ltmuls  28148  bdayfinbndlem1  28479  ax5seglem2  29018  axcontlem2  29054  fusgrfis  29419  3cyclfrgrrn  30377  isgrpoi  30590  imsmetlem  30782  nmcvcn  30787  ipval2  30799  lnocoi  30849  nmlno0lem  30885  nmblolbii  30891  blometi  30895  blocnilem  30896  blocni  30897  ipasslem1  30923  ipasslem2  30924  ipasslem4  30926  ipasslem5  30927  ipasslem8  30929  ipblnfi  30947  ip2eqi  30948  ubthlem1  30962  htthlem  31009  h2hmetdval  31070  axhvcom-zf  31075  axhis1-zf  31086  axhis4-zf  31089  hvm1neg  31124  hvsub4  31129  hvsubass  31136  hvsubdistr2  31142  hv2times  31153  hvsubcan  31166  hvsubcan2  31167  his2sub  31184  norm-i  31221  normpyc  31238  hhip  31269  hhph  31270  norm1exi  31342  hhssabloilem  31353  hhssnv  31356  hhshsslem2  31360  hhssmetdval  31369  shscli  31409  shunssi  31460  shsleji  31462  shsidmi  31476  spanunsni  31671  h1datomi  31673  spansncvi  31744  pjss2i  31772  pjssmii  31773  pjocini  31790  homullid  31892  honegdi  31901  ho2times  31911  nmopge0  32003  nmopgt0  32004  nmfnge0  32019  lnopaddi  32063  lnopmuli  32064  lnopsubi  32066  hmopbdoptHIL  32080  nmbdoplbi  32116  nmcoplbi  32120  nmophmi  32123  lnopconi  32126  lnfnaddi  32135  lnfnsubi  32138  nmbdfnlbi  32141  nmcfnlbi  32144  lnfnconi  32147  imaelshi  32150  cnlnadjlem2  32160  cnlnadjlem7  32165  nmoptrii  32186  nmopcoi  32187  adjcoi  32192  nmopcoadji  32193  bracnlnval  32206  leopmul  32226  opsqrlem1  32232  opsqrlem6  32237  hmopidmpji  32244  sto2i  32329  strlem1  32342  atcveq0  32440  atcv0eq  32471  atomli  32474  atcvati  32478  atcvat3i  32488  cdjreui  32524  cdj1i  32525  xdiv0  33009  xdivpnfrp  33013  mhmhmeotmd  34093  rezh  34135  qqhucn  34158  blsconn  35448  cnllysconn  35449  sate0fv0  35621  prv0  35634  sinccvglem  35876  opnrebl2  36525  ptrecube  37963  poimirlem6  37969  poimirlem7  37970  poimirlem29  37992  poimirlem30  37993  opnmbllem0  37999  mblfinlem3  38002  mblfinlem4  38003  ismblfin  38004  voliunnfl  38007  ftc1anclem5  38040  ftc1anclem7  38042  ftc1anclem8  38043  ftc1anc  38044  heiborlem7  38160  rrnequiv  38178  ismrer1  38181  el3v1  38573  preuniqval  38839  cnaddcom  39440  lcmineqlem1  42490  sn-ltaddpos  42920  mapco2  43169  mzpaddmpt  43195  mzpmulmpt  43196  zindbi  43400  mpaaeu  43604  tfsconcat0b  43800  eel000cT  45155  eel0TT  45156  supminfxr  45918  fmtno4prmfac  48055  pgn4cyclex  48622  aacllem  50296