Theorem mp3an1 1450

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

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

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 1088

This theorem is referenced by:  mp3an12  1453  mp3an1i  1456  mp3anl1  1457  mp3an  1463  mp3an2i  1468  mp3an3an  1469  onint  7766  tfrlem9  8353  oaord1  8515  oaword2  8517  oawordeulem  8518  oa00  8523  omword1  8537  omword2  8538  omlimcl  8542  oeoelem  8562  nnaordex  8602  naddword1  8655  undom  9029  rexdif1enOLD  9123  sucdom2  9167  enp1iOLD  9225  fodomfi  9261  fodomfib  9280  dffi3  9382  unbnn3  9612  ttrcltr  9669  frmin  9702  frrlem16  9711  pwdjuen  10135  zorn2  10459  zornn0  10461  ttukey  10471  brdom7disj  10484  brdom6disj  10485  muladd11  11344  negsubdi  11478  mulneg1  11614  ltaddpos  11668  addge01  11688  reccl  11844  recid  11851  recid2  11852  div0  11870  recdiv2  11895  divdiv23zi  11935  ltmul12a  12038  lemul12a  12040  mulgt1OLD  12041  ltmulgt11  12042  gt0div  12049  ge0div  12050  lediv12a  12076  ledivp1  12085  ltdiv23i  12107  ledivp1i  12108  ltdivp1i  12109  infm3  12142  8th4div3  12402  gtndiv  12611  nn0ind  12629  xrre2  13130  2resupmax  13148  qsqueeze  13161  xmulpnf1  13234  xlemul1a  13248  ioorebas  13412  elfz0ubfz0  13593  le2sq2  14100  expubnd  14143  crreczi  14193  bccl  14287  hashbc  14418  wrdred1hash  14526  ccatlid  14551  shftfval  15036  sgnp  15056  sqreulem  15326  binom1p  15797  fallrisefac  15991  efsub  16068  efi4p  16105  sinadd  16132  cosadd  16133  demoivreALT  16169  rpnnen2lem4  16185  odd2np1  16311  opoe  16333  omoe  16334  opeo  16335  omeo  16336  divalglem4  16366  divalglem9  16371  gcdcllem3  16471  gcdadd  16496  algcvgblem  16547  isprm3  16653  1arith2  16899  vdwap0  16947  vdwap1  16948  ipolt  18494  smndex1sgrp  18835  f1otrspeq  19377  rmodislmod  20836  cnfldneg  21307  cnflddiv  21312  cnflddivOLD  21313  cnfldmulg  21315  cnfldexp  21316  zringsub  21365  zringmulg  21366  zringsubgval  21380  remulg  21516  resubgval  21518  thlleval  21607  mplsubrglem  21913  evls1rhm  22209  iccordt  23101  bl2ioo  24680  xrsblre  24700  iccntr  24710  icccmplem3  24713  reconnlem2  24716  opnreen  24720  mpomulcn  24758  iccpnfcnv  24842  cnllycmp  24855  pcoptcl  24921  ismbl2  25428  cmmbl  25435  nulmbl  25436  unmbl  25438  voliunlem2  25452  ioombl1  25463  opnmbllem  25502  mbfima  25531  ellimc3  25780  limcflf  25782  coe1termlem  26163  dvnply2  26195  dvnply  26196  reeff1o  26357  sinperlem  26389  resinf1o  26445  logeftb  26492  logge0  26514  efopn  26567  loglesqrt  26671  logrec  26673  xrlimcnp  26878  ppinncl  27084  chtrpcl  27085  bposlem2  27196  bposlem8  27202  lgsdir2  27241  1lgs  27251  nosupno  27615  nosupbday  27617  noinfno  27630  noinfbday  27632  noetasuplem4  27648  lrrecfr  27850  sltmul  28039  ax5seglem2  28856  axcontlem2  28892  fusgrfis  29257  3cyclfrgrrn  30215  isgrpoi  30427  imsmetlem  30619  nmcvcn  30624  ipval2  30636  lnocoi  30686  nmlno0lem  30722  nmblolbii  30728  blometi  30732  blocnilem  30733  blocni  30734  ipasslem1  30760  ipasslem2  30761  ipasslem4  30763  ipasslem5  30764  ipasslem8  30766  ipblnfi  30784  ip2eqi  30785  ubthlem1  30799  htthlem  30846  h2hmetdval  30907  axhvcom-zf  30912  axhis1-zf  30923  axhis4-zf  30926  hvm1neg  30961  hvsub4  30966  hvsubass  30973  hvsubdistr2  30979  hv2times  30990  hvsubcan  31003  hvsubcan2  31004  his2sub  31021  norm-i  31058  normpyc  31075  hhip  31106  hhph  31107  norm1exi  31179  hhssabloilem  31190  hhssnv  31193  hhshsslem2  31197  hhssmetdval  31206  shscli  31246  shunssi  31297  shsleji  31299  shsidmi  31313  spanunsni  31508  h1datomi  31510  spansncvi  31581  pjss2i  31609  pjssmii  31610  pjocini  31627  homullid  31729  honegdi  31738  ho2times  31748  nmopge0  31840  nmopgt0  31841  nmfnge0  31856  lnopaddi  31900  lnopmuli  31901  lnopsubi  31903  hmopbdoptHIL  31917  nmbdoplbi  31953  nmcoplbi  31957  nmophmi  31960  lnopconi  31963  lnfnaddi  31972  lnfnsubi  31975  nmbdfnlbi  31978  nmcfnlbi  31981  lnfnconi  31984  imaelshi  31987  cnlnadjlem2  31997  cnlnadjlem7  32002  nmoptrii  32023  nmopcoi  32024  adjcoi  32029  nmopcoadji  32030  bracnlnval  32043  leopmul  32063  opsqrlem1  32069  opsqrlem6  32074  hmopidmpji  32081  sto2i  32166  strlem1  32179  atcveq0  32277  atcv0eq  32308  atomli  32311  atcvati  32315  atcvat3i  32325  cdjreui  32361  cdj1i  32362  xdiv0  32849  xdivpnfrp  32853  mhmhmeotmd  33917  rezh  33959  qqhucn  33982  blsconn  35231  cnllysconn  35232  sate0fv0  35404  prv0  35417  sinccvglem  35659  opnrebl2  36309  ptrecube  37614  poimirlem6  37620  poimirlem7  37621  poimirlem29  37643  poimirlem30  37644  opnmbllem0  37650  mblfinlem3  37653  mblfinlem4  37654  ismblfin  37655  voliunnfl  37658  ftc1anclem5  37691  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  heiborlem7  37811  rrnequiv  37829  ismrer1  37832  el3v1  38212  cnaddcom  38965  lcmineqlem1  42017  sn-ltaddpos  42441  mapco2  42703  mzpaddmpt  42729  mzpmulmpt  42730  zindbi  42935  mpaaeu  43139  tfsconcat0b  43335  eel000cT  44692  eel0TT  44693  supminfxr  45460  fmtno4prmfac  47573  pgn4cyclex  48116  aacllem  49790