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  7737  tfrlem9  8318  oaord1  8480  oaword2  8482  oawordeulem  8483  oa00  8488  omword1  8502  omword2  8503  omlimcl  8507  oeoelem  8528  nnaordex  8568  naddword1  8621  undom  8997  sucdom2  9131  fodomfi  9216  fodomfib  9233  dffi3  9338  unbnn3  9572  ttrcltr  9629  frmin  9665  frrlem16  9674  pwdjuen  10096  zorn2  10420  zornn0  10422  ttukey  10432  brdom7disj  10445  brdom6disj  10446  muladd11  11307  negsubdi  11441  mulneg1  11577  ltaddpos  11631  addge01  11651  reccl  11807  recid  11814  recid2  11815  div0  11833  recdiv2  11858  divdiv23zi  11898  ltmul12a  12001  lemul12a  12003  mulgt1OLD  12004  ltmulgt11  12005  gt0div  12012  ge0div  12013  lediv12a  12039  ledivp1  12048  ltdiv23i  12070  ledivp1i  12071  ltdivp1i  12072  infm3  12105  8th4div3  12365  gtndiv  12573  nn0ind  12591  xrre2  13089  2resupmax  13107  qsqueeze  13120  xmulpnf1  13193  xlemul1a  13207  ioorebas  13371  elfz0ubfz0  13552  le2sq2  14062  expubnd  14105  crreczi  14155  bccl  14249  hashbc  14380  wrdred1hash  14488  ccatlid  14514  shftfval  14997  sgnp  15017  sqreulem  15287  binom1p  15758  fallrisefac  15952  efsub  16029  efi4p  16066  sinadd  16093  cosadd  16094  demoivreALT  16130  rpnnen2lem4  16146  odd2np1  16272  opoe  16294  omoe  16295  opeo  16296  omeo  16297  divalglem4  16327  divalglem9  16332  gcdcllem3  16432  gcdadd  16457  algcvgblem  16508  isprm3  16614  1arith2  16860  vdwap0  16908  vdwap1  16909  ipolt  18462  smndex1sgrp  18837  f1otrspeq  19380  rmodislmod  20885  cnfldneg  21354  cnflddiv  21359  cnflddivOLD  21360  cnfldmulg  21362  cnfldexp  21363  zringsub  21414  zringmulg  21415  zringsubgval  21429  remulg  21566  resubgval  21568  thlleval  21657  mplsubrglem  21963  evls1rhm  22270  iccordt  23162  bl2ioo  24740  xrsblre  24760  iccntr  24770  icccmplem3  24773  reconnlem2  24776  opnreen  24780  mpomulcn  24818  iccpnfcnv  24902  cnllycmp  24915  pcoptcl  24981  ismbl2  25488  cmmbl  25495  nulmbl  25496  unmbl  25498  voliunlem2  25512  ioombl1  25523  opnmbllem  25562  mbfima  25591  ellimc3  25840  limcflf  25842  coe1termlem  26223  dvnply2  26255  dvnply  26256  reeff1o  26417  sinperlem  26449  resinf1o  26505  logeftb  26552  logge0  26574  efopn  26627  loglesqrt  26731  logrec  26733  xrlimcnp  26938  ppinncl  27144  chtrpcl  27145  bposlem2  27256  bposlem8  27262  lgsdir2  27301  1lgs  27311  nosupno  27675  nosupbday  27677  noinfno  27690  noinfbday  27692  noetasuplem4  27708  lrrecfr  27943  ltmuls  28136  bdayfinbndlem1  28467  ax5seglem2  29006  axcontlem2  29042  fusgrfis  29407  3cyclfrgrrn  30365  isgrpoi  30577  imsmetlem  30769  nmcvcn  30774  ipval2  30786  lnocoi  30836  nmlno0lem  30872  nmblolbii  30878  blometi  30882  blocnilem  30883  blocni  30884  ipasslem1  30910  ipasslem2  30911  ipasslem4  30913  ipasslem5  30914  ipasslem8  30916  ipblnfi  30934  ip2eqi  30935  ubthlem1  30949  htthlem  30996  h2hmetdval  31057  axhvcom-zf  31062  axhis1-zf  31073  axhis4-zf  31076  hvm1neg  31111  hvsub4  31116  hvsubass  31123  hvsubdistr2  31129  hv2times  31140  hvsubcan  31153  hvsubcan2  31154  his2sub  31171  norm-i  31208  normpyc  31225  hhip  31256  hhph  31257  norm1exi  31329  hhssabloilem  31340  hhssnv  31343  hhshsslem2  31347  hhssmetdval  31356  shscli  31396  shunssi  31447  shsleji  31449  shsidmi  31463  spanunsni  31658  h1datomi  31660  spansncvi  31731  pjss2i  31759  pjssmii  31760  pjocini  31777  homullid  31879  honegdi  31888  ho2times  31898  nmopge0  31990  nmopgt0  31991  nmfnge0  32006  lnopaddi  32050  lnopmuli  32051  lnopsubi  32053  hmopbdoptHIL  32067  nmbdoplbi  32103  nmcoplbi  32107  nmophmi  32110  lnopconi  32113  lnfnaddi  32122  lnfnsubi  32125  nmbdfnlbi  32128  nmcfnlbi  32131  lnfnconi  32134  imaelshi  32137  cnlnadjlem2  32147  cnlnadjlem7  32152  nmoptrii  32173  nmopcoi  32174  adjcoi  32179  nmopcoadji  32180  bracnlnval  32193  leopmul  32213  opsqrlem1  32219  opsqrlem6  32224  hmopidmpji  32231  sto2i  32316  strlem1  32329  atcveq0  32427  atcv0eq  32458  atomli  32461  atcvati  32465  atcvat3i  32475  cdjreui  32511  cdj1i  32512  xdiv0  33012  xdivpnfrp  33016  mhmhmeotmd  34086  rezh  34128  qqhucn  34151  blsconn  35440  cnllysconn  35441  sate0fv0  35613  prv0  35626  sinccvglem  35868  opnrebl2  36517  ptrecube  37823  poimirlem6  37829  poimirlem7  37830  poimirlem29  37852  poimirlem30  37853  opnmbllem0  37859  mblfinlem3  37862  mblfinlem4  37863  ismblfin  37864  voliunnfl  37867  ftc1anclem5  37900  ftc1anclem7  37902  ftc1anclem8  37903  ftc1anc  37904  heiborlem7  38020  rrnequiv  38038  ismrer1  38041  el3v1  38433  preuniqval  38699  cnaddcom  39300  lcmineqlem1  42351  sn-ltaddpos  42775  mapco2  43024  mzpaddmpt  43050  mzpmulmpt  43051  zindbi  43255  mpaaeu  43459  tfsconcat0b  43655  eel000cT  45010  eel0TT  45011  supminfxr  45775  fmtno4prmfac  47885  pgn4cyclex  48439  aacllem  50113