Theorem mpan9 516

Description: Modus ponens conjoining dissimilar antecedents. (Contributed by NM, 1-Feb-2008.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Hypotheses

Ref	Expression
mpan9.1	⊢ (𝜑 → 𝜓)
mpan9.2	⊢ (𝜒 → (𝜓 → 𝜃))

Assertion

Ref	Expression
mpan9	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Proof of Theorem mpan9

Step	Hyp	Ref	Expression
1		mpan9.1	. . 3 ⊢ (𝜑 → 𝜓)
2		mpan9.2	. . 3 ⊢ (𝜒 → (𝜓 → 𝜃))
3	1, 2	syl5 35	. 2 ⊢ (𝜒 → (𝜑 → 𝜃))
4	3	impcom 413	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

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

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

This theorem is used by:  sylan  592  vtocl2gf  3532  vtocl3gf  3533  vtocl2g  3534  vtocl3g  3535  sbcthdv  3755  elinsn  4671  swopolem  5569  wereu  5647  funssres  6582  dffv2  6978  fmptcof  7129  fnprb  7212  fntpb  7213  fliftfuns  7320  isorel  7332  oveqrspc2v  7445  caovclg  7611  caovcomg  7614  caovassg  7617  caovcang  7620  caovordig  7624  caovordg  7626  caovdig  7633  caovdirg  7636  caofidlcan  7729  peano5  7903  dmfexALT  7918  frpoins3xp3g  8151  fvmpocurryd  8281  qliftfuns  8818  nneneq  9214  ttrcltr  9710  ttrclselem2  9720  frins3  9752  setrec2fun  9966  cfslb  10337  hsmexlem4  10500  axdc3lem2  10522  axdc4lem  10526  adderpq  11034  mulerpq  11035  ltordlem  11834  lble  12262  uz11  12983  xrsupsslem  13430  xrinfmsslem  13431  xrsupss  13432  xrinfmss  13433  fseqsupubi  14114  hashbclem  14590  ccatass  14727  swrdswrd  14847  swrdccatin1  14867  swrdccatin2  14871  cshwcsh2id  14972  wwlktovf  15102  isercolllem1  15825  caucvgb  15840  zsum  15877  fsum  15879  fsumf1o  15882  fsumcvg2  15886  isummulc2  15921  fsum2dlem  15929  fsumcom2  15933  fsumshftm  15940  fsum0diag2  15942  fsum00  15958  fsumrlim  15971  o1fsum  15973  isumshft  16001  clim2prod  16050  ntrivcvgfvn0  16061  zprod  16097  fprod  16101  fprodf1o  16106  prodss  16107  fprodser  16109  fprodcllemf  16118  fprodm1s  16130  fprodp1s  16131  fprodabs  16134  fprod2dlem  16140  fprodcom2  16144  fprodefsum  16254  mod2eq1n2dvds  16510  sumeven  16550  sumodd  16551  lcmfun  16813  pythagtriplem4  16990  pcmptdvds  17065  prslem  18464  posi  18484  dlatmjdi  18690  lidrididd  18844  grpidinv2  19201  qsxpid  19380  ghmlin  19428  cntzmhm2  19549  dprdss  20238  dprd2d2  20253  omndadd  20335  srgrz  20426  srglz  20427  ringinvnz1ne0  20524  rrgeq0i  20944  lmodlema  21133  islmodd  21134  lsscl  21210  lsslss  21229  lspdisjb  21397  lsslinds  22130  assalem  22158  fvmptnn04if  23160  chfacfscmulgsum  23171  chfacfpmmulgsum  23175  ssnei2  23427  t1ficld  23638  t1sep2  23680  unconn  23740  1stcclb  23755  ptbasfi  23893  tx1stc  23962  qtoptop2  24011  r0sep  24060  ustincl  24520  ustdiag  24521  ustinvel  24522  ustexhalf  24523  psmet0  24620  psmettri2  24621  prdsdsf  24679  prdsxmet  24681  cncfi  25208  ovolfiniun  25815  mbfimaopnlem  25969  limciun  26207  dvcn  26234  dvmptfsum  26288  dvfsumle  26334  dvfsumabs  26336  dvfsumlem3  26341  itgsubst  26362  fsumvma  27533  dchrelbasd  27559  dchrisumlem3  27811  ssslts1  28152  ssslts2  28153  madeval2  28212  elmade  28236  axcontlem9  29543  usgruspgrb  29757  uspgrloopvtxel  30090  umgr2v2evtxel  30096  clwwlknonex2lem2  30692  loop1cycl  30737  3spthd  30770  grpoass  31098  lnolin  31349  elnlfn  32523  strlem4  32849  hstrlem4  32857  atmd  32994  nn0min  33405  slmdlema  33757  esumcvg  34711  measxun2  34836  sibfima  34963  bnj110  35481  bnj594  35535  bnj1491  35680  cvmcov  36007  mrsubcn  36263  dfon2lem5  36529  ifscgr  36789  nn0prpw  37091  neibastop2lem  37128  axnulregtco  37248  tr0el  37253  dfttc4  37298  bj-restb  37995  poimirlem25  38543  poimirlem32  38550  mbfresfi  38564  totbndss  38691  ghomlinOLD  38802  rngodi  38818  rngodir  38819  rngoass  38820  rngohomadd  38883  rngohommul  38884  crngocom  38915  idladdcl  38933  idllmulcl  38934  idlrmulcl  38935  exlimddvf  39033  oposlem  40219  cvlexch1  40365  hlsuprexch  40418  lautle  41121  elrfirn2  43686  wepwsolem  44028  kelac1  44049  islssfg2  44057  lnmlssfg  44066  onov0suclim  44260  relprel  45919  ovolval5lem3  47633  2elfz3nn0  48355  2elfz2melfz  48357  icceuelpartlem  48486  wtgoldbnnsum4prm  48869  bgoldbnnsum3prm  48871  bgoldbtbnd  48876  gpgedg2iv  49134  pgnbgreunbgrlem3  49185  pgnbgreunbgrlem6  49191  oppcendc  50095