Theorem mpan9 281

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 32	. 2 ⊢ (𝜒 → (𝜑 → 𝜃))
4	3	impcom 125	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem is referenced by:  sylan  283  vtocl2gf  2866  vtocl3gf  2867  vtoclegft  2878  sbcthdv  3046  disji2  4080  exmid1stab  4298  swopolem  4402  funssres  5369  fvmptssdm  5731  fmptcof  5814  fliftfuns  5938  isorel  5948  oveqrspc2v  6044  caovclg  6174  caovcomg  6177  caovassg  6180  caovcang  6183  caovordig  6187  caovordg  6189  caovdig  6196  caovdirg  6199  qliftfuns  6787  nneneq  7042  supmoti  7191  exmidonfinlem  7403  recexprlemopl  7844  recexprlemopu  7846  cauappcvgprlemladdrl  7876  caucvgsrlemcl  8008  caucvgsrlemfv  8010  caucvgsr  8021  suplocsrlempr  8026  ltordlem  8661  lble  9126  uz11  9778  seq3caopr3  10752  ccatass  11184  swrdswrd  11285  swrdccatin1  11305  swrdccatin2  11309  climcaucn  11911  sumdc  11918  fsum3  11947  fsumf1o  11950  fsum3cvg2  11954  isummulc2  11986  fsum2dlemstep  11994  fisumcom2  11998  fsumshftm  12005  fisum0diag2  12007  fsum00  12022  isumshft  12050  clim2prod  12099  prodmodclem2  12137  zproddc  12139  fprodseq  12143  fprodf1o  12148  prodssdc  12149  fprodm1s  12161  fprodp1s  12162  fprodcllemf  12173  fprodabs  12176  fprod2dlemstep  12182  fprodcom2fi  12186  dvdsprm  12708  pythagtriplem4  12840  pcmptdvds  12917  lidrididd  13464  grpidinv2  13640  ghmlin  13834  srgrz  13996  srglz  13997  ringinvnz1ne0  14061  rrgeq0i  14277  lmodlema  14305  islmodd  14306  lsslss  14394  ssnei2  14880  psmet0  15050  psmettri2  15051  cncfi  15301  dvcn  15423  dvmptfsum  15448  usgruspgrben  16036  wlk1walkdom  16209  clwwlknonex2lem2  16288  nninfsellemdc  16612