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  5939  isorel  5949  oveqrspc2v  6045  caovclg  6175  caovcomg  6178  caovassg  6181  caovcang  6184  caovordig  6188  caovordg  6190  caovdig  6197  caovdirg  6200  qliftfuns  6788  nneneq  7043  supmoti  7192  exmidonfinlem  7404  recexprlemopl  7845  recexprlemopu  7847  cauappcvgprlemladdrl  7877  caucvgsrlemcl  8009  caucvgsrlemfv  8011  caucvgsr  8022  suplocsrlempr  8027  ltordlem  8662  lble  9127  uz11  9779  seq3caopr3  10754  ccatass  11189  swrdswrd  11290  swrdccatin1  11310  swrdccatin2  11314  climcaucn  11916  sumdc  11923  fsum3  11953  fsumf1o  11956  fsum3cvg2  11960  isummulc2  11992  fsum2dlemstep  12000  fisumcom2  12004  fsumshftm  12011  fisum0diag2  12013  fsum00  12028  isumshft  12056  clim2prod  12105  prodmodclem2  12143  zproddc  12145  fprodseq  12149  fprodf1o  12154  prodssdc  12155  fprodm1s  12167  fprodp1s  12168  fprodcllemf  12179  fprodabs  12182  fprod2dlemstep  12188  fprodcom2fi  12192  dvdsprm  12714  pythagtriplem4  12846  pcmptdvds  12923  lidrididd  13470  grpidinv2  13646  ghmlin  13840  srgrz  14003  srglz  14004  ringinvnz1ne0  14068  rrgeq0i  14284  lmodlema  14312  islmodd  14313  lsslss  14401  ssnei2  14887  psmet0  15057  psmettri2  15058  cncfi  15308  dvcn  15430  dvmptfsum  15455  usgruspgrben  16043  wlk1walkdom  16216  clwwlknonex2lem2  16295  nninfsellemdc  16638