Theorem mp3an1 1478

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  mp3an12  1481  mp3an1i  1484  mp3anl1  1485  mp3an  1491  mp3an2i  1496  mp3an3an  1497  onint  7825  tfrlem9  8418  oaord1  8584  oaword2  8586  oawordeulem  8587  oa00  8592  omword1  8606  omword2  8607  omlimcl  8611  oeoelem  8632  nnaordex  8672  naddword1  8726  undom  9109  sucdom2  9243  fodomfi  9329  fodomfib  9345  dffi3  9447  unbnn3  9684  ttrcltr  9741  frmin  9777  frrlem16  9786  pwdjuen  10284  zorn2  10608  zornn0  10610  ttukey  10620  brdom7disj  10634  brdom6disj  10635  muladd11  11504  negsubdi  11638  mulneg1  11776  ltaddpos  11830  addge01  11850  reccl  12005  recid  12012  recid2  12013  div0  12029  recdiv2  12054  divdiv23zi  12094  ltmul12a  12197  lemul12a  12199  ltmulgt11  12200  gt0div  12207  ge0div  12208  lediv12a  12234  ledivp1  12243  ltdiv23i  12265  ledivp1i  12266  ltdivp1i  12267  infm3  12300  8th4div3  12590  gtndiv  12800  nn0ind  12818  xrre2  13324  2resupmax  13342  qsqueeze  13355  xmulpnf1  13428  xlemul1a  13442  ioorebas  13606  elfz0ubfz0  13790  le2sq2  14302  expubnd  14345  crreczi  14396  bccl  14490  hashbc  14622  wrdred1hash  14730  ccatlid  14756  shftfval  15249  sgnp  15269  sqreulem  15553  binom1p  16026  fallrisefac  16218  efsub  16294  efi4p  16331  sinadd  16358  cosadd  16359  demoivreALT  16395  rpnnen2lem4  16411  odd2np1  16537  opoe  16559  omoe  16560  opeo  16561  omeo  16562  divalglem4  16592  divalglem9  16597  gcdcllem3  16697  gcdadd  16724  algcvgblem  16778  isprm3  16884  1arith2  17132  vdwap0  17180  vdwap1  17181  ipolt  18735  smndex1sgrp  19133  f1otrspeq  19688  rmodislmod  21232  cnfldneg  21731  cnflddiv  21735  cnfldmulg  21737  cnfldexp  21738  zringsub  21788  zringmulg  21789  zringsubgval  21803  remulg  21940  resubgval  21942  thlleval  22031  mplsubrglem  22338  evls1rhm  22667  iccordt  23559  bl2ioo  25138  xrsblre  25158  iccntr  25168  icccmplem3  25171  reconnlem2  25174  opnreen  25178  mpomulcn  25215  iccpnfcnv  25292  cnllycmp  25304  pcoptcl  25369  ismbl2  25875  cmmbl  25882  nulmbl  25883  unmbl  25885  voliunlem2  25899  ioombl1  25910  opnmbllem  25949  mbfima  25978  ellimc3  26226  limcflf  26228  coe1termlem  26604  dvnply2  26635  dvnply  26636  reeff1o  26801  sinperlem  26836  resinf1o  26891  logeftb  26938  logge0  26960  efopn  27013  loglesqrt  27116  logrec  27118  xrlimcnp  27323  ppinncl  27528  chtrpcl  27529  bposlem2  27639  bposlem8  27645  lgsdir2  27684  1lgs  27694  nosupno  28087  nosupbday  28089  noinfno  28102  noinfbday  28104  noetasuplem4  28120  lrrecfr  28356  ltmuls  28549  bdayfinbndlem1  28880  ax5seglem2  29534  axcontlem2  29570  fusgrfis  29938  3cyclfrgrrn  30914  isgrpoi  31127  imsmetlem  31319  nmcvcn  31324  ipval2  31336  lnocoi  31386  nmlno0lem  31422  nmblolbii  31428  blometi  31432  blocnilem  31433  blocni  31434  ipasslem1  31460  ipasslem2  31461  ipasslem4  31463  ipasslem5  31464  ipasslem8  31466  ipblnfi  31484  ip2eqi  31485  ubthlem1  31499  htthlem  31546  h2hmetdval  31607  axhvcom-zf  31612  axhis1-zf  31623  axhis4-zf  31626  hvm1neg  31661  hvsub4  31666  hvsubass  31673  hvsubdistr2  31679  hv2times  31690  hvsubcan  31703  hvsubcan2  31704  his2sub  31721  norm-i  31758  normpyc  31775  hhip  31806  hhph  31807  norm1exi  31879  hhssabloilem  31890  hhssnv  31893  hhshsslem2  31897  hhssmetdval  31906  shscli  31946  shunssi  31997  shsleji  31999  shsidmi  32013  spanunsni  32208  h1datomi  32210  spansncvi  32281  pjss2i  32309  pjssmii  32310  pjocini  32327  homullid  32429  honegdi  32438  ho2times  32448  nmopge0  32540  nmopgt0  32541  nmfnge0  32556  lnopaddi  32600  lnopmuli  32601  lnopsubi  32603  hmopbdoptHIL  32617  nmbdoplbi  32653  nmcoplbi  32657  nmophmi  32660  lnopconi  32663  lnfnaddi  32672  lnfnsubi  32675  nmbdfnlbi  32678  nmcfnlbi  32681  lnfnconi  32684  imaelshi  32687  cnlnadjlem2  32697  cnlnadjlem7  32702  nmoptrii  32723  nmopcoi  32724  adjcoi  32729  nmopcoadji  32730  bracnlnval  32743  leopmul  32763  opsqrlem1  32769  opsqrlem6  32774  hmopidmpji  32781  sto2i  32866  strlem1  32879  atcveq0  32977  atcv0eq  33008  atomli  33011  atcvati  33015  atcvat3i  33025  cdjreui  33061  cdj1i  33062  xdiv0  33562  xdivpnfrp  33566  mhmhmeotmd  34626  rezh  34668  qqhucn  34691  omeueq  35793  dfk12  36011  dfk22  36012  dfk32  36013  jk1k2k3  36017  prconf1acwevd  36047  blsconn  36175  cnllysconn  36176  sate0fv0  36348  prv0  36361  sinccvglem  36603  opnrebl2  37286  ptrecube  38729  poimirlem6  38735  poimirlem7  38736  poimirlem29  38758  poimirlem30  38759  opnmbllem0  38765  mblfinlem3  38768  mblfinlem4  38769  ismblfin  38770  voliunnfl  38773  ftc1anclem5  38806  ftc1anclem7  38808  ftc1anclem8  38809  ftc1anc  38810  heiborlem7  38942  rrnequiv  38960  ismrer1  38963  el3v1  39353  preuniqval  39619  cnaddcom  40220  lcmineqlem1  43270  sn-ltaddpos  43708  mapco2  43917  mzpaddmpt  43943  mzpmulmpt  43944  zindbi  44144  mpaaeu  44342  tfsconcat0b  44538  eel000cT  45874  eel0TT  45875  supminfxr  46677  fmtno4prmfac  48860  pgn4cyclex  49427  aacllem  51217