Theorem mp3an1 1476

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∧ w3a 1102

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 401  df-3an 1104

This theorem is used by:  mp3an12  1479  mp3an1i  1482  mp3anl1  1483  mp3an  1489  mp3an2i  1494  mp3an3an  1495  onint  7787  tfrlem9  8370  oaord1  8534  oaword2  8536  oawordeulem  8537  oa00  8542  omword1  8556  omword2  8557  omlimcl  8561  oeoelem  8582  nnaordex  8622  naddword1  8676  undom  9051  sucdom2  9185  fodomfi  9270  fodomfib  9286  dffi3  9389  unbnn3  9626  ttrcltr  9683  frmin  9719  frrlem16  9728  pwdjuen  10172  zorn2  10496  zornn0  10498  ttukey  10508  brdom7disj  10521  brdom6disj  10522  muladd11  11386  negsubdi  11520  mulneg1  11656  ltaddpos  11710  addge01  11730  reccl  11885  recid  11892  recid2  11893  div0  11909  recdiv2  11934  divdiv23zi  11974  ltmul12a  12077  lemul12a  12079  ltmulgt11  12080  gt0div  12087  ge0div  12088  lediv12a  12114  ledivp1  12123  ltdiv23i  12145  ledivp1i  12146  ltdivp1i  12147  infm3  12180  8th4div3  12470  gtndiv  12679  nn0ind  12697  xrre2  13202  2resupmax  13220  qsqueeze  13233  xmulpnf1  13306  xlemul1a  13320  ioorebas  13484  elfz0ubfz0  13667  le2sq2  14178  expubnd  14221  crreczi  14271  bccl  14365  hashbc  14497  wrdred1hash  14605  ccatlid  14631  shftfval  15114  sgnp  15134  sqreulem  15418  binom1p  15892  fallrisefac  16086  efsub  16162  efi4p  16199  sinadd  16226  cosadd  16227  demoivreALT  16263  rpnnen2lem4  16279  odd2np1  16405  opoe  16427  omoe  16428  opeo  16429  omeo  16430  divalglem4  16460  divalglem9  16465  gcdcllem3  16565  gcdadd  16590  algcvgblem  16641  isprm3  16747  1arith2  16994  vdwap0  17042  vdwap1  17043  ipolt  18597  smndex1sgrp  18976  f1otrspeq  19523  rmodislmod  21062  cnfldneg  21559  cnflddiv  21563  cnfldmulg  21565  cnfldexp  21566  zringsub  21616  zringmulg  21617  zringsubgval  21631  remulg  21768  resubgval  21770  thlleval  21859  mplsubrglem  22164  evls1rhm  22493  iccordt  23382  bl2ioo  24960  xrsblre  24980  iccntr  24990  icccmplem3  24993  reconnlem2  24996  opnreen  25000  mpomulcn  25037  iccpnfcnv  25114  cnllycmp  25126  pcoptcl  25191  ismbl2  25697  cmmbl  25704  nulmbl  25705  unmbl  25707  voliunlem2  25721  ioombl1  25732  opnmbllem  25771  mbfima  25800  ellimc3  26049  limcflf  26051  coe1termlem  26426  dvnply2  26459  dvnply  26460  reeff1o  26621  sinperlem  26656  resinf1o  26712  logeftb  26759  logge0  26781  efopn  26834  loglesqrt  26937  logrec  26939  xrlimcnp  27144  ppinncl  27349  chtrpcl  27350  bposlem2  27460  bposlem8  27466  lgsdir2  27505  1lgs  27515  nosupno  27878  nosupbday  27880  noinfno  27893  noinfbday  27895  noetasuplem4  27911  lrrecfr  28147  ltmuls  28340  bdayfinbndlem1  28671  ax5seglem2  29290  axcontlem2  29326  fusgrfis  29691  3cyclfrgrrn  30648  isgrpoi  30861  imsmetlem  31053  nmcvcn  31058  ipval2  31070  lnocoi  31120  nmlno0lem  31156  nmblolbii  31162  blometi  31166  blocnilem  31167  blocni  31168  ipasslem1  31194  ipasslem2  31195  ipasslem4  31197  ipasslem5  31198  ipasslem8  31200  ipblnfi  31218  ip2eqi  31219  ubthlem1  31233  htthlem  31280  h2hmetdval  31341  axhvcom-zf  31346  axhis1-zf  31357  axhis4-zf  31360  hvm1neg  31395  hvsub4  31400  hvsubass  31407  hvsubdistr2  31413  hv2times  31424  hvsubcan  31437  hvsubcan2  31438  his2sub  31455  norm-i  31492  normpyc  31509  hhip  31540  hhph  31541  norm1exi  31613  hhssabloilem  31624  hhssnv  31627  hhshsslem2  31631  hhssmetdval  31640  shscli  31680  shunssi  31731  shsleji  31733  shsidmi  31747  spanunsni  31942  h1datomi  31944  spansncvi  32015  pjss2i  32043  pjssmii  32044  pjocini  32061  homullid  32163  honegdi  32172  ho2times  32182  nmopge0  32274  nmopgt0  32275  nmfnge0  32290  lnopaddi  32334  lnopmuli  32335  lnopsubi  32337  hmopbdoptHIL  32351  nmbdoplbi  32387  nmcoplbi  32391  nmophmi  32394  lnopconi  32397  lnfnaddi  32406  lnfnsubi  32409  nmbdfnlbi  32412  nmcfnlbi  32415  lnfnconi  32418  imaelshi  32421  cnlnadjlem2  32431  cnlnadjlem7  32436  nmoptrii  32457  nmopcoi  32458  adjcoi  32463  nmopcoadji  32464  bracnlnval  32477  leopmul  32497  opsqrlem1  32503  opsqrlem6  32508  hmopidmpji  32515  sto2i  32600  strlem1  32613  atcveq0  32711  atcv0eq  32742  atomli  32745  atcvati  32749  atcvat3i  32759  cdjreui  32795  cdj1i  32796  xdiv0  33259  xdivpnfrp  33263  mhmhmeotmd  34326  rezh  34368  qqhucn  34391  blsconn  35744  cnllysconn  35745  sate0fv0  35917  prv0  35930  sinccvglem  36172  opnrebl2  36860  ptrecube  38299  poimirlem6  38305  poimirlem7  38306  poimirlem29  38328  poimirlem30  38329  opnmbllem0  38335  mblfinlem3  38338  mblfinlem4  38339  ismblfin  38340  voliunnfl  38343  ftc1anclem5  38376  ftc1anclem7  38378  ftc1anclem8  38379  ftc1anc  38380  heiborlem7  38496  rrnequiv  38514  ismrer1  38517  el3v1  38907  preuniqval  39173  cnaddcom  39774  lcmineqlem1  42824  sn-ltaddpos  43255  mapco2  43474  mzpaddmpt  43500  mzpmulmpt  43501  zindbi  43701  mpaaeu  43905  tfsconcat0b  44101  eel000cT  45439  eel0TT  45440  supminfxr  46206  fmtno4prmfac  48352  pgn4cyclex  48919  aacllem  50649