Theorem mp3an1 1477

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  1480  mp3an1i  1483  mp3anl1  1484  mp3an  1490  mp3an2i  1495  mp3an3an  1496  onint  7792  tfrlem9  8377  oaord1  8541  oaword2  8543  oawordeulem  8544  oa00  8549  omword1  8563  omword2  8564  omlimcl  8568  oeoelem  8589  nnaordex  8629  naddword1  8683  undom  9066  sucdom2  9200  fodomfi  9285  fodomfib  9301  dffi3  9404  unbnn3  9641  ttrcltr  9698  frmin  9734  frrlem16  9743  pwdjuen  10187  zorn2  10511  zornn0  10513  ttukey  10523  brdom7disj  10537  brdom6disj  10538  muladd11  11407  negsubdi  11541  mulneg1  11677  ltaddpos  11731  addge01  11751  reccl  11906  recid  11913  recid2  11914  div0  11930  recdiv2  11955  divdiv23zi  11995  ltmul12a  12098  lemul12a  12100  ltmulgt11  12101  gt0div  12108  ge0div  12109  lediv12a  12135  ledivp1  12144  ltdiv23i  12166  ledivp1i  12167  ltdivp1i  12168  infm3  12201  8th4div3  12491  gtndiv  12701  nn0ind  12719  xrre2  13224  2resupmax  13242  qsqueeze  13255  xmulpnf1  13328  xlemul1a  13342  ioorebas  13506  elfz0ubfz0  13689  le2sq2  14201  expubnd  14244  crreczi  14294  bccl  14388  hashbc  14520  wrdred1hash  14628  ccatlid  14654  shftfval  15145  sgnp  15165  sqreulem  15449  binom1p  15922  fallrisefac  16116  efsub  16192  efi4p  16229  sinadd  16256  cosadd  16257  demoivreALT  16293  rpnnen2lem4  16309  odd2np1  16435  opoe  16457  omoe  16458  opeo  16459  omeo  16460  divalglem4  16490  divalglem9  16495  gcdcllem3  16595  gcdadd  16620  algcvgblem  16671  isprm3  16777  1arith2  17024  vdwap0  17072  vdwap1  17073  ipolt  18627  smndex1sgrp  19021  f1otrspeq  19575  rmodislmod  21115  cnfldneg  21612  cnflddiv  21616  cnfldmulg  21618  cnfldexp  21619  zringsub  21669  zringmulg  21670  zringsubgval  21684  remulg  21821  resubgval  21823  thlleval  21912  mplsubrglem  22219  evls1rhm  22548  iccordt  23440  bl2ioo  25019  xrsblre  25039  iccntr  25049  icccmplem3  25052  reconnlem2  25055  opnreen  25059  mpomulcn  25096  iccpnfcnv  25173  cnllycmp  25185  pcoptcl  25250  ismbl2  25756  cmmbl  25763  nulmbl  25764  unmbl  25766  voliunlem2  25780  ioombl1  25791  opnmbllem  25830  mbfima  25859  ellimc3  26108  limcflf  26110  coe1termlem  26485  dvnply2  26518  dvnply  26519  reeff1o  26680  sinperlem  26715  resinf1o  26771  logeftb  26818  logge0  26840  efopn  26893  loglesqrt  26996  logrec  26998  xrlimcnp  27203  ppinncl  27408  chtrpcl  27409  bposlem2  27519  bposlem8  27525  lgsdir2  27564  1lgs  27574  nosupno  27937  nosupbday  27939  noinfno  27952  noinfbday  27954  noetasuplem4  27970  lrrecfr  28206  ltmuls  28399  bdayfinbndlem1  28730  ax5seglem2  29372  axcontlem2  29408  fusgrfis  29776  3cyclfrgrrn  30752  isgrpoi  30965  imsmetlem  31157  nmcvcn  31162  ipval2  31174  lnocoi  31224  nmlno0lem  31260  nmblolbii  31266  blometi  31270  blocnilem  31271  blocni  31272  ipasslem1  31298  ipasslem2  31299  ipasslem4  31301  ipasslem5  31302  ipasslem8  31304  ipblnfi  31322  ip2eqi  31323  ubthlem1  31337  htthlem  31384  h2hmetdval  31445  axhvcom-zf  31450  axhis1-zf  31461  axhis4-zf  31464  hvm1neg  31499  hvsub4  31504  hvsubass  31511  hvsubdistr2  31517  hv2times  31528  hvsubcan  31541  hvsubcan2  31542  his2sub  31559  norm-i  31596  normpyc  31613  hhip  31644  hhph  31645  norm1exi  31717  hhssabloilem  31728  hhssnv  31731  hhshsslem2  31735  hhssmetdval  31744  shscli  31784  shunssi  31835  shsleji  31837  shsidmi  31851  spanunsni  32046  h1datomi  32048  spansncvi  32119  pjss2i  32147  pjssmii  32148  pjocini  32165  homullid  32267  honegdi  32276  ho2times  32286  nmopge0  32378  nmopgt0  32379  nmfnge0  32394  lnopaddi  32438  lnopmuli  32439  lnopsubi  32441  hmopbdoptHIL  32455  nmbdoplbi  32491  nmcoplbi  32495  nmophmi  32498  lnopconi  32501  lnfnaddi  32510  lnfnsubi  32513  nmbdfnlbi  32516  nmcfnlbi  32519  lnfnconi  32522  imaelshi  32525  cnlnadjlem2  32535  cnlnadjlem7  32540  nmoptrii  32561  nmopcoi  32562  adjcoi  32567  nmopcoadji  32568  bracnlnval  32581  leopmul  32601  opsqrlem1  32607  opsqrlem6  32612  hmopidmpji  32619  sto2i  32704  strlem1  32717  atcveq0  32815  atcv0eq  32846  atomli  32849  atcvati  32853  atcvat3i  32863  cdjreui  32899  cdj1i  32900  xdiv0  33361  xdivpnfrp  33365  mhmhmeotmd  34424  rezh  34466  qqhucn  34489  blsconn  35810  cnllysconn  35811  sate0fv0  35983  prv0  35996  sinccvglem  36238  opnrebl2  36927  ptrecube  38356  poimirlem6  38362  poimirlem7  38363  poimirlem29  38385  poimirlem30  38386  opnmbllem0  38392  mblfinlem3  38395  mblfinlem4  38396  ismblfin  38397  voliunnfl  38400  ftc1anclem5  38433  ftc1anclem7  38435  ftc1anclem8  38436  ftc1anc  38437  heiborlem7  38554  rrnequiv  38572  ismrer1  38575  el3v1  38965  preuniqval  39231  cnaddcom  39832  lcmineqlem1  42882  sn-ltaddpos  43328  mapco2  43547  mzpaddmpt  43573  mzpmulmpt  43574  zindbi  43774  mpaaeu  43978  tfsconcat0b  44174  eel000cT  45512  eel0TT  45513  supminfxr  46279  fmtno4prmfac  48462  pgn4cyclex  49029  aacllem  50759