Theorem 3expia 1133

Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3expia	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Proof of Theorem 3expia

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3expb 1132	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	expr 460	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1099

This theorem is referenced by:  ad5ant125OLD  1382  mp3an3  1470  3gencl  3496  vtocl3gaf  3543  vtocl3ga  3544  moi  3679  disji  5082  disjord  5086  3optocl  5740  sossfld  6167  f1oresrab  7104  f1cdmsn  7261  soisores  7306  isomin  7316  isofrlem  7319  ovmpos  7539  ov2gf  7540  ndmovord  7581  nnsuc  7859  poxp  8102  frpoins3xp3g  8115  brtpos  8209  dfsmo2  8312  smoiun  8326  smoord  8330  smogt  8332  omeulem1  8545  omeu  8548  oewordi  8555  uniinqs  8773  mapvalg  8811  pmvalg  8812  elmapg  8814  xpdom3  9041  mapdom3  9115  sdomdomtrfi  9163  domsdomtrfi  9164  php  9169  php3  9171  nndomog  9175  onomeneq  9176  sucdom  9182  unxpdomlem3  9196  isinf  9203  f1finf1o  9211  isfinite2  9236  prfi  9262  ordiso  9458  cnfcom3clem  9654  r111  9727  tskwe  9902  pr2ne  9955  infxpenlem  9963  dfac8alem  9979  infdif  10158  infdif2  10159  cff1  10209  coflim  10212  cfslbn  10218  cfslb2n  10219  cofsmo  10220  cfsmolem  10221  cfcoflem  10223  fin23lem27  10279  isf32lem9  10312  isf34lem6  10331  axcc2lem  10387  domtriomlem  10393  axdc4lem  10406  zorn2lem2  10448  axdclem2  10471  konigthlem  10520  gchen1  10577  gchen2  10578  gchpwdom  10622  gchaleph  10623  winainflem  10645  tskcard  10733  gruiun  10751  gruen  10764  intgru  10766  grudomon  10769  grur1a  10771  grutsk1  10773  nqereu  10881  nqereq  10887  ltsonq  10921  prlem934  10985  reclem3pr  11001  1re  11175  axsup  11252  addlid  11360  recex  11813  lemul1a  12039  lt2msq  12071  fimaxre2  12131  indpi1  12203  zdiv  12637  zextlt  12641  prime  12648  uzind2  12660  fzind  12665  lbzbi  12931  qbtwnxr  13197  qextltlem  13199  xralrple  13202  xltneg  13214  xlt2add  13257  supxrgtmnf  13326  ixxub  13364  ixxlb  13365  ioo0  13368  ico0  13389  ioc0  13390  icc0  13391  iocssre  13425  icossre  13426  iccssre  13427  fzen  13540  expclzlem  14090  expaddz  14113  expmulz  14115  hashgadd  14384  hashunsngx  14400  hashgt23el  14431  elovmpowrd  14565  pfxnd0  14696  ccatopth2  14724  pfxccatin12  14740  cshf1  14817  shftuz  15076  sgn3da  15105  sgnnbi  15108  sgnpbi  15109  cau3lem  15373  caubnd  15377  climuni  15570  lo1resb  15582  o1resb  15584  o1of2  15631  o1add  15632  o1mul  15633  o1sub  15634  ntrivcvgmul  15923  eflt  16140  moddvds  16288  dvdscmulr  16309  dvdsmulcr  16310  dvdsle  16335  divalglem8  16425  divalgb  16429  ndvdssub  16434  bitsfzo  16460  gcdcllem1  16524  gcdcllem3  16526  dvdsgcd  16569  nn0rppwr  16586  nn0expgcd  16589  lcmgcdlem  16631  lcmfeq0b  16655  qredeu  16683  isprm3  16708  prmdvdsexpr  16743  prmexpb  16745  eulerthlem2  16808  fermltl  16810  coprimeprodsq  16835  pythagtrip  16861  pcprendvds  16867  pcpremul  16870  pcdvdsb  16896  pc2dvds  16906  4sqlem12  16983  4sqlem18  16989  vdwlem10  17017  cshwshashlem3  17124  xpsrnbas  17592  ismred  17621  mrieqv2d  17662  iscatd  17696  isfuncd  17889  fthestrcsetc  18173  fthsetcestrc  18188  poslubd  18434  dirtr  18625  mulgaddcom  19131  ghmrn  19260  pmtrprfv3  19485  mndodcongi  19574  oddvdsnn0  19575  oddvds  19578  odcl2  19596  odhash3  19607  gexdvds  19615  pgpfi  19636  lsmss1b  19697  lsmss2b  19699  efgsrel  19765  efgred  19779  cntzcmn  19871  cyggenod  19915  lt6abl  19926  gsumcom2  20006  pgpfac1lem2  20108  pgpfac1lem3  20110  dvdsunit  20415  unitmulclb  20417  irredrmul  20463  isabvd  20849  lmodvsdi  20940  lss0cl  21002  islbs3  21213  lbsextlem2  21217  xrsdsreclblem  21453  psrbaglefi  21966  mvrf1  22025  coe1fzgsumd  22355  gsummoncoe1  22359  evl1gsumd  22408  scmataddcl  22564  scmatsubcl  22565  mdetunilem9  22668  mdetuni0  22669  mdetmul  22671  m2cpmrngiso  22806  pm2mpf1  22847  opnnei  23168  neindisj2  23171  cncls2  23321  cncls  23322  cnntr  23323  cnpresti  23336  cnprest  23337  lmcnp  23352  isreg2  23425  ordthauslem  23431  unconn  23477  2ndc1stc  23499  kgen2ss  23603  ptclsg  23663  cnmptcom  23726  kqfvima  23778  hmeof1o  23812  fbncp  23887  fbfinnfr  23889  trfbas2  23891  isufil2  23956  ufprim  23957  trufil  23958  filufint  23968  hausflim  24029  flimrest  24031  flimcls  24033  cnpfcf  24089  alexsubALT  24099  tmdgsum  24143  opnsubg  24156  cldsubg  24159  qustgpopn  24168  tsmsxp  24203  blpnf  24445  blssps  24472  blss  24473  blssec  24483  neibl  24549  prdsxmslem2  24577  xrsmopn  24861  metnrm  24911  climcncf  24950  iccpnfhmeo  24995  xrhmeo  24996  bndth  25008  cphsqrtcl3  25237  iscau2  25327  iscmet3lem2  25342  bcthlem5  25378  bcth3  25381  ishl2  25420  ivthlem1  25501  cmmbl  25584  iundisj2  25599  voliunlem2  25601  mbfaddlem  25710  itg2itg1  25786  itg2seq  25792  itg2mulclem  25796  cnplimc  25937  dvres2  25962  deg1nn0clb  26138  deg1lt0  26139  deg1ge  26146  plypf1  26260  plyadd  26265  plymul  26266  coeeu  26273  dgrub2  26283  coeidlem  26285  coeid3  26288  coemullem  26298  coe11  26301  coemulhi  26302  coemulc  26303  dgreq0  26313  dgrlt  26314  dgradd2  26316  vieta1lem2  26363  tanord1  26590  tanord  26591  logccne0  26631  cxpeq0  26731  cxpmul2z  26744  cxpcn3lem  26800  rtprmirr  26813  relogbzcl  26827  angpieqvd  26884  o1cxp  27027  scvxcvx  27038  chtublem  27263  bposlem3  27338  lgsqr  27403  2sqnn  27491  dchrisumlema  27540  dchrisumlem2  27542  ostth2lem3  27687  nosepon  27717  noextenddif  27720  nolesgn2o  27723  nogesgn1o  27725  nosepne  27732  nodense  27744  onnolt  28347  onlts  28348  oniso  28352  bdayn0p1  28450  bdayn0sf1o  28451  tghilberti2  28795  inagswap  28998  f1otrg  29028  brbtwn2  29063  axpasch  29099  axcontlem4  29125  axcontlem5  29126  upgredg2vtx  29299  usgredg2vtxeuALT  29380  sizusglecusg  29621  upgredginwlk  29793  frgrwopreg1  30477  frgrwopreg2  30478  frgrregorufrg  30485  lpni  30640  ipasslem5  30995  htthlem  31077  omlsii  31563  spansni  31717  spansneleq  31730  elspansn4  31733  sumspansn  31809  homco1  31961  homulass  31962  mdsl0  32470  ssdmd1  32473  ssdmd2  32474  cvdmd  32497  chirredlem2  32551  atdmd  32558  atmd2  32560  disjif  32738  iundisj2f  32750  isoun  32865  preiman0  32873  padct  32881  iocinioc2  32942  iundisj2fi  32960  archiabllem1a  33332  archiabllem2a  33335  slmdvsdi  33356  ordtconnlem1  34182  measinblem  34478  measres  34480  measdivcstALTV  34483  mbfmco2  34523  orvclteinc  34734  bnj605  35163  bnj607  35172  bnj964  35199  bnj1033  35225  bnj1128  35246  bnj1137  35251  bnj1136  35253  bnj1413  35291  bnj60  35318  rankfilimb  35359  r1filim  35361  fineqvac  35373  fineqvnttrclselem3  35380  fineqvnttrclse  35381  vonf1oonfo  35419  cusgredgex  35433  subgrwlk  35443  acycgr1v  35460  cvmlift2lem10  35623  msubvrs  35871  wsuclem  36134  dfrdg4  36262  brcolinear2  36369  brsegle2  36420  nn0prpw  36644  ntruni  36648  clsint2  36650  fnessref  36678  fnemeet2  36688  fnejoin2  36690  limsucncmpi  36766  ee7.2aOLD  36782  bj-idreseq  37615  dissneqlem  37795  isbasisrelowllem1  37810  isbasisrelowllem2  37811  icoreclin  37812  poimirlem9  38089  poimirlem30  38110  poimirlem32  38112  areacirc  38173  filbcmb  38200  mettrifi  38217  heiborlem8  38278  heiborlem10  38280  heibor  38281  riscer  38448  igenval2  38526  eldisjim3  39275  eldisjs6  39400  lshpcmp  39573  eqlkr  39684  lkrlsp2  39688  lkrshp  39690  cvrnbtwn2  39860  cvlexch3  39917  cvlexch4N  39918  cvlatexchb1  39919  cvlsupr3  39929  exatleN  39989  cvratlem  40006  atcvrj2b  40017  cvrat3  40027  cvrat4  40028  athgt  40041  ps-1  40062  ps-2  40063  3atlem5  40072  3at  40075  llnneat  40099  llnmlplnN  40124  lplnneat  40130  lplnnelln  40131  islpln2a  40133  lplnriaN  40135  lplnribN  40136  lplnexllnN  40149  2llnjaN  40151  lvolnle3at  40167  lvolneatN  40173  lvolnelln  40174  lvolnelpln  40175  islvol2aN  40177  dalem62  40319  pmapglb2N  40356  pmapglb2xN  40357  lncmp  40368  paddasslem14  40418  paddasslem15  40419  pmod2iN  40434  hlmod1i  40441  pclfinclN  40535  osumcllem8N  40548  pexmidlem4N  40558  pl42lem1N  40564  pl42lem4N  40567  lhpexle1  40593  lhpexle2lem  40594  lhpmcvr5N  40612  lhpmcvr6N  40613  ltrneq  40734  trlnidatb  40762  cdleme0ex2N  40809  cdleme27a  40952  cdleme17d3  41081  cdlemeg46gfre  41117  cdleme48gfv1  41121  cdlemeg49lebilem  41124  cdlemf2  41147  cdlemf  41148  cdlemfnid  41149  trlord  41154  cdlemg31c  41284  cdlemg35  41298  trlcone  41313  tendoeq2  41359  cdlemj3  41408  cdlemk26b-3  41490  cdlemk33N  41494  cdleml3N  41563  cdlemn  41797  dih1dimb2  41826  dihord5apre  41847  dihmeetlem1N  41875  dihglblem5apreN  41876  dihglblem2N  41879  dihglblem3N  41880  dihmeetlem13N  41904  dihmeetlem15N  41906  dihatexv  41923  hdmap14lem12  42464  uzindd  42556  lcmineqlem1  42607  sticksstones1  42724  dvdsexpnn0  42904  frlmfzowrdb  43087  oddcomabszz  43482  jm2.19lem4  43530  fiuneneq  43730  idomsubgmo  43731  omcl2  43871  pwinfi3  44100  gneispa  44667  mnringmulrcld  44765  grumnudlem  44822  ismnushort  44838  binomcxplemnn0  44886  addrcom  45011  int3  45149  suctrALT  45362  suctrALTcf  45458  suctrALT3  45460  chordthmALT  45469  iunconnlem2  45471  relpmin  45489  relpfrlem  45490  stoweidlem26  46561  stoweidlem34  46569  issald  46868  goldbachth  48117  nprmdvdsfacm1  48194  grlimgrtri  48586  nnsgrp  48760  ply1mulgsumlem1  48969  lubsscl  49542  glbsscl  49543