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  7744  tfrlem9  8324  oaord1  8486  oaword2  8488  oawordeulem  8489  oa00  8494  omword1  8508  omword2  8509  omlimcl  8513  oeoelem  8534  nnaordex  8574  naddword1  8627  undom  9003  sucdom2  9137  fodomfi  9222  fodomfib  9239  dffi3  9344  unbnn3  9580  ttrcltr  9637  frmin  9673  frrlem16  9682  pwdjuen  10104  zorn2  10428  zornn0  10430  ttukey  10440  brdom7disj  10453  brdom6disj  10454  muladd11  11316  negsubdi  11450  mulneg1  11586  ltaddpos  11640  addge01  11660  reccl  11816  recid  11823  recid2  11824  div0  11842  recdiv2  11868  divdiv23zi  11908  ltmul12a  12011  lemul12a  12013  mulgt1OLD  12014  ltmulgt11  12015  gt0div  12022  ge0div  12023  lediv12a  12049  ledivp1  12058  ltdiv23i  12080  ledivp1i  12081  ltdivp1i  12082  infm3  12115  8th4div3  12397  gtndiv  12606  nn0ind  12624  xrre2  13122  2resupmax  13140  qsqueeze  13153  xmulpnf1  13226  xlemul1a  13240  ioorebas  13404  elfz0ubfz0  13586  le2sq2  14097  expubnd  14140  crreczi  14190  bccl  14284  hashbc  14415  wrdred1hash  14523  ccatlid  14549  shftfval  15032  sgnp  15052  sqreulem  15322  binom1p  15796  fallrisefac  15990  efsub  16067  efi4p  16104  sinadd  16131  cosadd  16132  demoivreALT  16168  rpnnen2lem4  16184  odd2np1  16310  opoe  16332  omoe  16333  opeo  16334  omeo  16335  divalglem4  16365  divalglem9  16370  gcdcllem3  16470  gcdadd  16495  algcvgblem  16546  isprm3  16652  1arith2  16899  vdwap0  16947  vdwap1  16948  ipolt  18501  smndex1sgrp  18879  f1otrspeq  19422  rmodislmod  20925  cnfldneg  21378  cnflddiv  21382  cnfldmulg  21384  cnfldexp  21385  zringsub  21435  zringmulg  21436  zringsubgval  21450  remulg  21587  resubgval  21589  thlleval  21678  mplsubrglem  21982  evls1rhm  22287  iccordt  23179  bl2ioo  24757  xrsblre  24777  iccntr  24787  icccmplem3  24790  reconnlem2  24793  opnreen  24797  mpomulcn  24834  iccpnfcnv  24911  cnllycmp  24923  pcoptcl  24988  ismbl2  25494  cmmbl  25501  nulmbl  25502  unmbl  25504  voliunlem2  25518  ioombl1  25529  opnmbllem  25568  mbfima  25597  ellimc3  25846  limcflf  25848  coe1termlem  26223  dvnply2  26253  dvnply  26254  reeff1o  26412  sinperlem  26444  resinf1o  26500  logeftb  26547  logge0  26569  efopn  26622  loglesqrt  26725  logrec  26727  xrlimcnp  26932  ppinncl  27137  chtrpcl  27138  bposlem2  27248  bposlem8  27254  lgsdir2  27293  1lgs  27303  nosupno  27667  nosupbday  27669  noinfno  27682  noinfbday  27684  noetasuplem4  27700  lrrecfr  27935  ltmuls  28128  bdayfinbndlem1  28459  ax5seglem2  28998  axcontlem2  29034  fusgrfis  29399  3cyclfrgrrn  30356  isgrpoi  30569  imsmetlem  30761  nmcvcn  30766  ipval2  30778  lnocoi  30828  nmlno0lem  30864  nmblolbii  30870  blometi  30874  blocnilem  30875  blocni  30876  ipasslem1  30902  ipasslem2  30903  ipasslem4  30905  ipasslem5  30906  ipasslem8  30908  ipblnfi  30926  ip2eqi  30927  ubthlem1  30941  htthlem  30988  h2hmetdval  31049  axhvcom-zf  31054  axhis1-zf  31065  axhis4-zf  31068  hvm1neg  31103  hvsub4  31108  hvsubass  31115  hvsubdistr2  31121  hv2times  31132  hvsubcan  31145  hvsubcan2  31146  his2sub  31163  norm-i  31200  normpyc  31217  hhip  31248  hhph  31249  norm1exi  31321  hhssabloilem  31332  hhssnv  31335  hhshsslem2  31339  hhssmetdval  31348  shscli  31388  shunssi  31439  shsleji  31441  shsidmi  31455  spanunsni  31650  h1datomi  31652  spansncvi  31723  pjss2i  31751  pjssmii  31752  pjocini  31769  homullid  31871  honegdi  31880  ho2times  31890  nmopge0  31982  nmopgt0  31983  nmfnge0  31998  lnopaddi  32042  lnopmuli  32043  lnopsubi  32045  hmopbdoptHIL  32059  nmbdoplbi  32095  nmcoplbi  32099  nmophmi  32102  lnopconi  32105  lnfnaddi  32114  lnfnsubi  32117  nmbdfnlbi  32120  nmcfnlbi  32123  lnfnconi  32126  imaelshi  32129  cnlnadjlem2  32139  cnlnadjlem7  32144  nmoptrii  32165  nmopcoi  32166  adjcoi  32171  nmopcoadji  32172  bracnlnval  32185  leopmul  32205  opsqrlem1  32211  opsqrlem6  32216  hmopidmpji  32223  sto2i  32308  strlem1  32321  atcveq0  32419  atcv0eq  32450  atomli  32453  atcvati  32457  atcvat3i  32467  cdjreui  32503  cdj1i  32504  xdiv0  32988  xdivpnfrp  32992  mhmhmeotmd  34071  rezh  34113  qqhucn  34136  blsconn  35426  cnllysconn  35427  sate0fv0  35599  prv0  35612  sinccvglem  35854  opnrebl2  36503  ptrecube  37941  poimirlem6  37947  poimirlem7  37948  poimirlem29  37970  poimirlem30  37971  opnmbllem0  37977  mblfinlem3  37980  mblfinlem4  37981  ismblfin  37982  voliunnfl  37985  ftc1anclem5  38018  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  heiborlem7  38138  rrnequiv  38156  ismrer1  38159  el3v1  38551  preuniqval  38817  cnaddcom  39418  lcmineqlem1  42468  sn-ltaddpos  42898  mapco2  43147  mzpaddmpt  43173  mzpmulmpt  43174  zindbi  43374  mpaaeu  43578  tfsconcat0b  43774  eel000cT  45129  eel0TT  45130  supminfxr  45892  fmtno4prmfac  48035  pgn4cyclex  48602  aacllem  50276